Merge branch 'master' into feature/instant-theorem#1
Open
batmeezy918 wants to merge 135 commits intomasterfrom
Open
Merge branch 'master' into feature/instant-theorem#1batmeezy918 wants to merge 135 commits intomasterfrom
batmeezy918 wants to merge 135 commits intomasterfrom
Conversation
Owner
batmeezy918
commented
Mar 21, 2026
batmeezy918
commented
…)kernels (leanprover-community#36481) Introduce two object properties `kernels` and `cokernels` as well as predicates `IsClosedUnderKernels` and `IsClosedUnderCokernels`. Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
… via projections (leanprover-community#34209) A Schauder basis is a fundamental concept in functional analysis, providing a way to represent every element of a Banach space as a unique convergent series. This PR adds the core structures, some theorems necessary to work with these bases and a characterization of a Schauder basis using projections. This PR is based on Chapter 1. from Albiac, F., & Kalton, N. J. (2016). Topics in Banach Space Theory. This is a first PR in a series of three aiming for Eberlein-Smulyan Theorem. The next one will contain theory of basic sequences and the final one will contain a proof of Eberlein-Smulyan Theorem using basic sequences. Co-authored-by: Michał Świętek <swietekmichal@proton.me>
…leanprover-community#35292) this is an analogue to `List.take_take`.
…-bound for the set's mex (leanprover-community#36539) This is a translation of `card_typein_min_le_mk` to be in terms of `α`.
…eanprover-community#36395) This PR marks `IntermediateField.toSubfield`, `Subalgebra.toSubring` and `Subalgebra.toSubmodule` as `implicit_reducible`, because these are all used to construct instances on substructures, and hence need to be reducible when unifying type classes. This allows removing at least 100 backwards compatability flags (possibly more because I haven't checked these exhaustively)
…community#35858) This PR does the following: - Use better variable names in the docs (instead of just variants of the letter `o`). - Remove mentions of things defined in other files, or specify that they are defined on other files.
…ile, and dropWhile (leanprover-community#36473) This PR adds missing proofs that several standard `List` operations are primitive recursive (Primrec), as well as a basic property of `tail` and `drop`. Specifically, it introduces: * `List.tail_iterate`: Applying `tail` to a list `n` times is equivalent to dropping `n` elements. * `Primrec.list_drop`: `List.drop` is primitive recursive. * `Primrec.list_take`: `List.take` is primitive recursive. * `Primrec.list_takeWhile`: `List.takeWhile` is primitive recursive. * `Primrec.list_dropWhile`: `List.dropWhile` is primitive recursive. These are basic computability properties for lists that were currently missing from `Mathlib.Computability.Primrec.List`. All proofs use standard combinators and `of_eq`. Co-authored-by: AlexeyMilovanov <almas239@gmail.com>
…pes agree at instances transparency (leanprover-community#36717) This PR improves how \`fast_instance%\` handles proof-valued constructor fields. Previously, proof fields were always wrapped in \`mkAuxTheorem\`, which creates a separate auxiliary theorem carrying the expected type. This is unnecessary when the proof's actual type already agrees with the expected type at instances transparency — in that case the proof can be assigned directly. The new behaviour: check whether the proof's type agrees with the expected type at instances transparency. If yes, assign directly. If no (indicating a binder type mismatch), wrap with \`mkAuxTheorem\` as before. This is a natural analogue of the data-field binder type checking that \`fast_instance%\` already performs, applied to proof fields. 🤖 Prepared with Claude Code
…cy` (leanprover-community#36791) These are just the ones that are freely removable because of earlier fixes.
…(X) (leanprover-community#30505) We prove Ostrowski's theorem for the field of rational functions `K(X)`, where `K` is any field. Co-authored-by: @xgenereux Co-authored-by: mariainesdff <mariainesdff@gmail.com> Co-authored-by: mariainesdff <mariaines.dff@gmail.com>
… faster (leanprover-community#35947) This experiment investigates the impact of replacing particularly heavy `aesop` calls with `grind`, specifically how this change affects the instruction count as measured by the benchmarking infrastructure. Trace profiling results (differences <30 ms considered measurement noise): * `Submonoid.mem_closure_image_one_lt_iff`: 125 ms before, 61 ms after 🎉 * `SimpleGraph.Connected.connected_delete_edge_of_not_isBridge`: 230 ms before, 51 ms after 🎉 * `SimpleGraph.Subgraph.IsMatching.exists_of_disjoint_sets_of_equiv`: 899 ms before, 666 ms after 🎉 * `SimpleGraph.IsCycles.existsUnique_ne_adj`: 855 ms before, 599 ms after 🎉 * `SimpleGraph.Walk.IsPath.isCycles_spanningCoe_toSubgraph_sup_edge`: 962 ms before, 619 ms after 🎉 * `SimpleGraph.IsAlternating.sup_edge`: 2854 ms before, 1615 ms after 🎉 * `SimpleGraph.Subgraph.IsPerfectMatching.symmDiff_of_isAlternating`: 3103 ms before, 1734 ms after 🎉 * `SimpleGraph.edgeSet_replaceVertex_of_not_adj`: 1525 ms before, 933 ms after 🎉 * `SimpleGraph.edgeSet_replaceVertex_of_adj`: 2194 ms before, 1605 ms after 🎉 * `SimpleGraph.tutte_exists_isPerfectMatching_of_near_matchings`: 3161 ms before, 1652 ms after 🎉 * `RootPairing.Base.sub_notMem_range_root`: 1025 ms before, 978 ms after 🎉 * `RootPairing.EmbeddedG2.mem_allRoots`: 3832 ms before, 3255 ms after 🎉 * `RootSystem.GeckConstruction.Lemmas.0.RootPairing.chainBotCoeff_mul_chainTopCoeff.aux_2`: 3572 ms before, 2631 ms after 🎉 * `isCompact_generateFrom`: 1987 ms before, 763 ms after 🎉 * `IsCompactOpenCovered.of_isCompact_of_forall_exists_isCompactOpenCovered`: 2279 ms before, 2009 ms after 🎉 * `UniformContinuousOn.comp_tendstoUniformly_eventually`: 416 ms before, 151 ms after 🎉 Profiled using `set_option trace.profiler true in`.
Issues were spotted and fixed by Codex.
Define a predicate stating that a stochastic process has independent increments. Prove an equivalent definition using sequences instead of `Fin`. Prove some basic invariance properties. Co-authored-by: @jvanwinden
…o` and `continuousOn_Ici/Iic_primitive_Ioi/Iio/Ici/Iic` (leanprover-community#34966) This PR proves: - `continuousWithinAt_Ici/Iic_primitive_Ioi/Iio` - `continuousOn_Ici/Iic_primitive_Ioi/Iio/Ici/Iic` - `integral_Ioi_sub_Ioi`, `integral_Ioi_sub_Ioi'`, `integral_Iio_sub_Iio`, `integral_Iio_sub_Iio'` - `Ioi_diff_Ioc` Co-authored-by: Deep0Thinking <Deep0Thinking@outlook.com>
…nder, and make a lemma protected (leanprover-community#36522) Add the namespace `Filter` to `lim` and `limUnder`, since the docstring for `lim` suggests that they were never intended to be placed in the namespace. Also make `MeasureTheory.StronglyMeasurable.limUnder` protected, to allow its proof to refer to `Filter.limUnder` as `limUnder`. See discussion here: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Rename.20lim.20to.20Filter.2Elim.3F/with/578862980
…eQuotients` instance (leanprover-community#36535) This instance was removed in leanprover-community#36395 for performance reasons. This PR restores the instance in a form that is more performant.
…insupp` (leanprover-community#36762) Introduce `coeff : R[M] → M →₀ R` and `ofCoeff : (M →₀ R) → R[M]` as a way to convert explicitly between `MonoidAlgebra` and `Finsupp` and thus avoid defeq abuse. These will be used more widely in future PRs.
…over-community#36801) Remove `erw` and `respectTransparency` in `imageSubobjectMap_arrow`.
…y#36413) This PR give a bit of speedup by cleaning up some `Function.Injective.` and `Function.Surjective.` instances. The main point is to put the arguments in the correct order in `{ ..., ... with }`, matching the order of the `extends` clause.
… to Mul (leanprover-community#36737) Co-authored-by: mariainesdff <mariaines.dff@gmail.com>
…or_eq_floor` (leanprover-community#36805) This PR weakens the `CommRing R` assumption on `Int.abs_sub_lt_one_of_floor_eq_floor` into `Ring R`.
…ver-community#36405) Derivative of modular forms, stems from [Sphere Packing project](https://github.com/thefundamentaltheor3m/Sphere-Packing-Lean). The major goal is two-fold: prove Ramanujan's identities and also prove that Serre derivative preserves modularity (first uses second). Co-authored-by: Jeremy Tan Jie Rui <54175463+Parcly-Taxel@users.noreply.github.com> Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> Co-authored-by: Hagb (Junyu Guo 郭俊余) <hagb@hagb.name> Co-authored-by: Harald Husum <harald.husum@gmail.com> Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com> Co-authored-by: Bryan Gin-ge Chen <5209952+bryangingechen@users.noreply.github.com> Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk> Co-authored-by: Jovan Gerbscheid <56355248+JovanGerb@users.noreply.github.com> Co-authored-by: Bolton Bailey <bolton.bailey@gmail.com> Co-authored-by: Bingyu Xia <71547343+BryceT233@users.noreply.github.com> Co-authored-by: Salvatore Mercuri <47568553+smmercuri@users.noreply.github.com> Co-authored-by: euprunin <178733547+euprunin@users.noreply.github.com> Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com> Co-authored-by: Thomas Browning <13339017+tb65536@users.noreply.github.com> Co-authored-by: Rémy Degenne <4094732+RemyDegenne@users.noreply.github.com> Co-authored-by: Whysoserioushah <109107491+Whysoserioushah@users.noreply.github.com> Co-authored-by: Yongxi (Aaron) Lin <97214596+CoolRmal@users.noreply.github.com> Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com> Co-authored-by: Alex Meiburg <alex.meiburg@gmail.com>
…t in `Walk.rotate` (leanprover-community#36800) It is annoying for it not to appear in the infoview. In general, no implicit data argument to a definition should be inferrable only through proof arguments.
Define the binomial distribution and compute the expectation, variance, conditional variance of a binomial random variable. From MiscYD
…er-community#36685) Resolving a TODO in the code. This also makes `PiLp.single` the simp-normal form, as opposite to `toLp _ (Pi.single _ _)` that was in the code.
…odDomain (leanprover-community#26985) This PR continues the work from leanprover-community#16743. Original PR: leanprover-community#16743
…27229) From FLT Co-authored-by: WilliamCoram <williamecoram@gmail.com>
…f `IsAntichain` to spell "a color class is an independent set" (leanprover-community#33252)
…5756) Co-authored-by: @AntoineChambert-Loir. Co-authored-by: mariainesdff <mariaines.dff@gmail.com>
…s under polynomial maps (leanprover-community#35940) We continue the development of height bounds for polynomial maps. Here we add the lower bound.
…mClass` (leanprover-community#36658) Let's use the `abbrev` if we already have it.
…prover-community#36680) Let `c₁` (resp. `c₂`) be a cokernel cofork for a morphism `f₁ : X₁ ⟶ Y₁` in a category `C₁` (resp. `f₂ : X₂ ⟶ Y₂` in `C₂`). Given a bifunctor `F : C₁ ⥤ C₂ ⥤ C`, we construct a cokernel cofork with point `(F.obj c₁.pt).obj c₂.pt` for the obvious morphism `(F.obj X₁).obj Y₂ ⨿ (F.obj Y₁).obj X₂ ⟶ (F.obj Y₁).obj Y₂`, and show that it is a colimit when the cokernel of `f₁` is preserved by `F.obj c₁.pt` and the cokernel of `f₂` is perserved by `F.flip.obj X₁` and `F.flip.obj Y₁`.
…plex Hilbert space (leanprover-community#29251) define standard subspaces of a complex Hilbert space: a standard subspace `S` of `H` is a closed real subspace `S` such that `S ⊓ i S = ⊥` and `S ⊔ i S = ⊤`. prove that the symplectic complement of `S` is again a standard subspace and the double symplectic complement is itself. motivation: one can define a closable operator `x + i y ↦ x - i y` and develop an analogue of the Tomita-Takesaki modular theory for von Neumann algebras. By considering inclusions of standard subspaces, one can obtain unitary representations of various Lie groups. https://ems.press/content/serial-article-files/48171 `#min_imports` does not give a correct set of imports. - [x] depends on: leanprover-community#29230 for `Lattice` `CompleteLattice` - [x] depends on: leanprover-community#29241 for the definition of `orthogonal` - [x] depends on: leanprover-community#29243 for `sup_orthogonal` - [x] depends on: leanprover-community#29235 for `mapEquiv` Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
…leanprover-community#35908) We redefine `solvableByRad F E` as the smallest intermediate field closed under n-th roots. This makes the predicate `IsSolvableByRad` redundant, and so we deprecate it. We also private/remove various auxiliary results, and change the statement of the Abel-Ruffini theorem to be about an element of the field, rather than the subtype.
…leanprover-community#36492) This PR slightly generalises the domain in `FinitePlaces.lean` from `RingOfIntegers K` to `R` such that `Module.Finite ℤ R` and `Module.Free ℤ R`. This enables these results to be applied equally to `O ℚ` and `ℤ` when `K = ℚ`. Many results in the file previously had the namespace `NumberField.RingOfIntegers.HeightOneSpectrum`. These results no longer directly use the type `NumberField.RingOfIntegers`, so this namespace has been renamed to `NumberField.HeightOneSpectrum` leading to deprecations. This PR does not remove any results, however some are moved around in the file to facilitate better namespacing and section variables. These movements are as follows: - `FinitePlace.embedding`, `FinitePlace.embedding_apply` and `instance : Valued.v.IsRankOneDiscrete` now appear at the top of the file, l. 92. - `FinitePlace`, `FinitePlace.mk`, `IsFinitePlace`, `FinitePlace.isFinitePlace`, `isFinitePlace_iff` appear later in the file starting l. 264. - `adicAbv_add_le_max`, `adicAbv_natCast_le_one`, `adicAbv_intCast_le_one` appear earlier in the file, at l. 164.
… extension and the restriction of scalars (leanprover-community#36599)
…over-community#36646) Some of the docstrings referenced Homotopy (from Algebra/Homology) instead of ContinuousMap.Homotopy. Co-authored-by: NoahW314 <noahwalker3.14@gmail.com>
…ver-community#36894) This PR changes the lemma hover for `to_fun` so that it shows up only on the `to_fun` keyword itself, and not also on the `(attr := ...)` part. As a result, you can now go to the definition of `to_fun` by clicking on the `(attr := ...)` part. This PR also fixes the bug reported in [#**mathlib4>to_fun names**](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/to_fun.20names/with/580441233) that the lemma hover doesn't show up in combination with `(attr := ...)`.
…anprover-community#36903) This PR replaces a slow `aesop_cat` call with an explicit proof. This speeds it up by more that 10x. The trace of the `aesop_cat` call looks incredibly suspicious. It is spending all the 5 seconds on a `<norm simp>` node, but inside that trace node, the nodes only add up to less than 0.5 seconds. So it is a mystery to me what `aesop` is doing during this extra time. This was identified in leanprover-community#36613
…ver-community#34573) `lake shake --keep-implied --keep-prefix --fix --only Mathlib.Analysis.Normed.Lp.SmoothApprox`, using a dev version of `shake`
…types (leanprover-community#35867) This PR defines `Sheaf.classifier J : Classifier (Sheaf J (Type (max u v))`, which is the last ingredient missing to sheaf categories being elementary topoi. adapted from: https://github.com/edegeltje/CwFTT/blob/591d4505390172ae70e1bc97544d293a35cc0b3f/CwFTT/Classifier/Sheaf.lean Co-authored-by: Edward van de Meent <edwardvdmeent@gmail.com>
Co-authored by : @AntoineChambert-Loir Co-authored-by: mariainesdff <mariaines.dff@gmail.com>
…36594) This PR rewrites the docstrings for the `lift` tactic, to make sure they are complete while not getting too long. The main change, apart from restructuring the bullet points to fit the style guide, is to treat the form `lift e to t with x`, where `e` is any expression, as the "general" form, and the case where `e` is a variable as a specialized form. Although it doesn't match the historical development, I think this is clearer for new users (since explaining `lift` without `with` as a special case can be done with only one line). Similarly, we separate `using` into its own bullet point. In this docstring I did not include the alternative form `lift e to t with x rfl`, since it is exactly equivalent to `lift e to to with x` as far as I can tell. I did include `lift e to t with x rfl h`, because it is useful for preserving the `using` hypothesis without naming the introduced equality. Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
…ommunity#36859) This PR (re)writes the docstrings for the `move_oper` tactic (and its alternatives `move_add`/`move_mul`) to consistently match the official style guide, to make sure it is complete while not getting too long. I decided to focus on the form `move_oper op [a]` first, since this allows us to explain the basic functionality while being quite general. After that we can specialize to `move_add`/`move_mul`/... Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
…nity#36861) This PR rewrites the docstrings for the `mod_cases` tactic, to make sure they are complete while not getting too long. The only real changes are to match the style guideline and for consistent terminology (write "hypothesis" instead of "assumption"). Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
…e iterated derivatives (leanprover-community#33275) We prove that Chebyshev polynomials maximized iterated derivatives at points x≥1.
…emmas (leanprover-community#36795) `coe_toWeakDual` and `coe_toStrongDual` stated equalities between bundled maps (`toWeakDual x' = x'`), which is not a useful `simp` normal form. This PR removes `@[simp]` from these lemmas and replaces them with pointwise `_apply` variants: - `toWeakDual_apply (x' : StrongDual R M) (y : M) : (toWeakDual x') y = x' y` - `toStrongDual_apply (x : WeakDual k E) (y : E) : (toStrongDual x) y = x y` These are the correct simp normal form, rewriting function application rather than bundled map equality. --> [](https://gitpod.io/from-referrer/)
…rover-community#36905) This PR removes some workarounds for `cat_disch` being slow, where it is not slow anymore.
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
](https://gitpod.io/from-referrer/){kind=link}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: c5231dcc0f
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| @@ -0,0 +1 @@ | |||
| Nat.add_comm a b | |||
There was a problem hiding this comment.
Any new .lean file under Mathlib/ is picked up by scripts/mk_all.lean when it regenerates Mathlib.lean, and .github/workflows/build_template.yml runs lake exe mk_all --check on every PR. This commit adds Mathlib.Algebra.InstantTheorem (and similarly Mathlib.Algebra.MathlibDemo / Mathlib.Algebra.MyNewProofs) without adding corresponding imports to Mathlib.lean, so the mk_all check will report Mathlib.lean as out of date and block the PR.
Useful? React with 👍 / 👎.
|
|
||
| # open PR | ||
| gh pr create --base leanprover-community:master \ | ||
| --head batmeezy918:feature/your-proofs \ |
There was a problem hiding this comment.
The branch is pushed to origin, but the PR is opened from batmeezy918:feature/your-proofs. That only works when the caller's origin remote is that exact GitHub account; for any other contributor, the push can succeed and gh pr create still targets a non-existent or unauthorized head branch. Using the current remote/user (or omitting --head) would make the helper usable outside one personal fork.
Useful? React with 👍 / 👎.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
20 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.