Sync upstream mathlib4 (2026-07-28, +25 commits) - #87
Merged
Merged
Conversation
…2119) The proofs produced by the `norm_det` / `eval_det` simproc (added in #42059) could not be checked from within a `module` because the generated proofs depended on kernel checking of equalities for definitions (`Array.ofFn`, and `certEntry`, `certIterStepEntry` from the Bird determinant certificate evaluator) which are not exposed. The existing tests in `MathlibTest/matrix.lean` did not detect this issue because it was not a `module` itself. This PR: * Fixes the issues resulting from non-exposed definitions * Makes the `MathlibTest/matrix.lean` file into a module * Adds proofs for the determinants of Cartan matrices `LinearAlgebra/Matrix/Cartan` using `norm_det` - showing that the simrproc can be used in mathlib modules. The function `normalizeDetFromEntries` generated a proof which related the matrix array literal to `Array.ofFn fun k => A k.divNat k.modNat` by an unchecked `=Q` equality. This cannot be checked by the kernel because `Array.ofFn` is not exposed. The solution here is to use `List.ofFn` instead, which is exposed. Similarly, the functions `certEntry` and `certIterStepEntry` in the Bird determinant certificate evaluator relied on definitional unfolding of `BirdDet.get` and `BirdDet.stepEntry` which are not exposed. The generated proofs now use the unfolding lemmas `BirdDet.get_eq` and `BirdDet.stepEntry_eq` instead.
Add `Quiver.Reachable a b`, the existence of a directed path from `a` to `b`, together with its basic preorder API (`@[refl]`/`@[trans]`) and `Path.reachable`/`Hom.reachable`. Unlike `SimpleGraph.Reachable`, this is only a preorder, not an equivalence, since quiver paths are directed; the symmetric notion is reachability in `Symmetrify V`. Co-authored-by: Runtian Zhou <rz169@duke.edu>
…#40724) Given a real inner product space `E`, we construct a canonical inner product on `⋀[ℝ]^n E` via the Gram determinant formula: on decomposable elements, `⟪v₁ ∧ ⋯ ∧ vₙ, w₁ ∧ ⋯ ∧ wₙ⟫ = det (⟪vⱼ, wᵢ⟫)ᵢⱼ`. There are two generalizations of this construction: Going from `ℝ` to `RCLike`, and getting rid of the `FiniteDimensional` assumption. Both would require some prerequisites, hence they are left as future work for now (see the future work section of the module docstring). Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
Causes no slowdowns Co-authored-by: Batixx <s59fpern@uni-bonn.de>
Add additive analogs of `FreeGroupBasis`/`IsFreeGroup` and apply `@[to_additive]` throughout the rest of the file.
… center of an inversion. (#36313) Co-authored-by: Oliver Nash <github@olivernash.org>
…Nat cast in intervals to intervals of floor and ceil functions (#41512) For a `FloorRing` (resp. `FloorSemiring`) `α`, we relate membership of a cast `↑n` in an interval of `α` to membership of the integer (resp. natural number) `n` in the corresponding interval with floor/ceil endpoints, for instance `Int.coe_mem_Ioc_iff : ↑n ∈ Set.Ioc a b ↔ n ∈ Set.Ioc ⌊a⌋ ⌊b⌋`. If the right-hand side is finite, we express them as `Finset` instead. Co-authored-by: Terence Tao <tao@math.ucla.edu> Co-authored-by: Oliver Nash <github@olivernash.org>
…ttice operations (#40269) From the exponential-ramsey project Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
…morphism (#40298)
Adds the `RingEquiv` analogues of the `RingHom.to{Nat,Int,Rat}AlgHom` / `RingHom.equivRatAlgHom` constructions, over `ℕ`, `ℤ` and `ℚ`:
- `RingEquiv.toNatAlgEquiv`, `RingEquiv.toIntAlgEquiv`, `RingEquiv.toRatAlgEquiv`: a `RingEquiv` is canonically an ℕ-, ℤ- or ℚ-algebra isomorphism.
- `ringEquivEquivNatAlgEquiv`, `ringEquivEquivIntAlgEquiv`, `ringEquivEquivRatAlgEquiv`: the corresponding equivalences `(R ≃+* S) ≃ (R ≃ₐ[·] S)`.
:robot: This PR was extracted from the [SKW project](https://github.com/xroblot/SKW) by Claude.
Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
…(#40282) The join of characteristic subgroups is characteristic.
Co-authored-by: Brian-Nugent <bnugent@uw.edu>
Under suitable assumptions, `Comma.fst/snd` jointly reflect (co)limits. These additions allow to simplify the definition `coneOfPreservesIsLimit` and its dual.
…p.Basic (#41616) This instance removes the commutativity assumption on k in the current instance Abelian (Rep k G) in Rep.Iso.
Co-authored-by: alreadydone <3064145+alreadydone@users.noreply.github.com>
The comment makes no sense any more: `noncomputable section` checks first if a def is computable, and only if not, makes it noncomputable. So `noncomputable section` wouldn't make a difference here (for an example where `noncomputable def` vs `noncomputable section` makes a difference see [#mathlib4 > noncomputable section @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/noncomputable.20section/near/609434583)). Looking at the git history, it used to be marked `noncomputable def`, but that was removed in #40091 without comment. This is not a performance issue any more, so the comment can just be removed. Co-authored-by: Batixx <s59fpern@uni-bonn.de>
…(#35349) Co-authored-by: Remy Degenne <remydegenne@gmail.com>
The new `IsApply` typeclasses allow many existing special-case `coe_xxx` lemmas to be unified; but the general lemmas currently do not have the simp tag. This tags them as simp. Other minor changes: - There were two lemmas with statements identical up to argument order: `FunLike.coe_smul` (directly written) and `FunLike.coe_smul'` (auto-generated by `to_additive`). I unified these using `to_additive existing`, with a deprecation alias for `FunLike.coe_smul'`. - Downstream code that uses `FunLike.coe_smul'` is adjusted appropriately (un-squeezing a couple of lengthy terminal `simp only`'s in the process). - One more specific simp lemma downstream (`ContinuousLinearMap.coe_pow'`) is removed, because `simp` can now prove it using the `FunLike` simp lemmas. A misnamed lemma in this file, `ContinuousLinearMap.coe_pow`, was re-named to `ContinuousLinearMap.toLinearMap_pow`. - There were just two simps (both in `Mathlib/Probability/Distributions/Gaussian/Basic.lean`) which broke, because they used an un-squeezed `simp` along with an additional explicitly provided lemma (not part of the default simp set) that conflicted with `FunLike.coe_zero`. These I fixed by explicitly removing `FunLike.coe_zero` from the simp set where necessary.
…homomorphisms (#42054)
This PR deprecates all definitions in differential geometry with underscores in their names, and renames it according to the naming convention. Co-authored-by: Batixx <s59fpern@uni-bonn.de>
Following up on the description of #40792, this removes additional uses of `Subrelation` now that #30526 has been merged.
This PR gives a direct proof of `Algebra.IsAlgebraic.finrank_of_isFractionRing` which avoids any additional assumptions beyond those required for the statement (including `Algebra.IsAlgebraic`). Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
…lter (#42135) Add two lemmas describing the edges of a finite simple graph `G` whose vertices all lie in a finset `s`.
$\pm I$ are primitive 4-th roots of unity. Arise from a personal project, and written with Claude Opus 5 + Fable 5. It is not clear for me if this is the best place to put this theorem (since the file is mostly about $\exp(2\pi I/n)$), but looks the closest choice. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> <!-- Your PR title will become the first line of the commit message. In this box, the text above the `---` (if not empty) will be appended to the commit message, and can be used to give additional context or details. Please leave a blank newline before the `---`, otherwise GitHub will format the text above it as a title. For details on the "pull request lifecycle" in mathlib, please see: https://leanprover-community.github.io/contribute/index.html In particular, note that most reviewers will only notice your PR if it passes the continuous integration checks. Please ask for help on https://leanprover.zulipchat.com if needed. When merging, all the commits will be squashed into a single commit listing all co-authors. Co-authors in the squash commit are gathered from two sources: First, all authors of commits to this PR branch are included. Thus, one way to add co-authors is to include at least one commit authored by each co-author among the commits in the pull request. If necessary, you may create empty commits to indicate co-authorship, using commands like so: git commit --author="Author Name <author@email.com>" --allow-empty -m "add Author Name as coauthor" Second, co-authors can also be listed in lines at the very bottom of the commit message (that is, directly before the `---`) using the following format: If you are moving or deleting declarations, please include these lines at the bottom of the commit message (before the `---`, and also before any "Co-authored-by" lines) using the following format: Moves: - Vector.* -> List.Vector.* - ... Deletions: - Nat.bit1_add_bit1 - ... Any other comments you want to keep out of the PR commit should go below the `---`, and placed outside this HTML comment, or else they will be invisible to reviewers. If this PR depends on other PRs, please list them below this comment, using the following format: - [ ] depends on: #abc [optional extra text] - [ ] depends on: #xyz [optional extra text] --> [](https://gitpod.io/from-referrer/) Co-authored-by: Author Name <author@email.com>
](https://gitpod.io/from-referrer/){kind=link}
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.
Automated daily sync from
leanprover-community/mathlib4@master.996c094298abe6682d90e374ffc84b6419b6d2ceAuto-merges to
masteronceCI (self-hosted)passes. Regenerateddaily until merged or until a conflict appears.
Note
Low Risk
Routine upstream library sync with additive APIs and deprecations; no auth or deployment surface, though renames may affect downstream imports until migrations land.
Overview
Automated sync from
leanprover-community/mathlib4(25 commits);Mathlib.leangains public imports for exterior-power inner products, convex-space affine maps, KL data processing, and floor/ceil interval finsets.New analysis & geometry:
ExteriorPower.leanbuilds a Gram-determinant inner product on⋀[ℝ]^n Eand an induced orthonormal basis;ConvexSpace.AffineMapbundles affine maps between convex spaces;ConvexOn.continuousOn_Ici/Ici/Ioc/Ico/Iccextend convexity-based continuity on real intervals; a Euclidean inversion tends to infinity at the center.Information theory & measure theory:
KullbackLeibler/DataProcessing.leanproves data processing for KL divergence (klDiv_map_le,klDiv_trim_le,klDiv_comp_right_le), reusing newConvexOnlemmas for Radon–Nikodym derivatives and conditional expectation.Algebra & category theory:
RingEquivgainstoNatAlgEquiv/toIntAlgEquiv/toRatAlgEquivand matching equivalences; characteristic subgroups are stable under sup/inf and (bi)sup/(bi)inf; comma categories getfstSndJointlyReflectLimit/fstSndJointlyReflectColimitand simpler limit proofs;Repis declared abelian via the action equivalence (moved fromRep/Iso).Combinatorics & linear algebra:
Quiver.Reachableand graphneighborSet/neighborFinsetlattice laws; finiteness/rank lemmas for localization and fraction rings (finrank_left_eq,finrank_eq); exceptional Cartan determinants proved vianorm_det;Complex.isPrimitiveRoot_I/neg_I.API hygiene: Many definitions renamed to camelCase with deprecations (manifold
ChartedSpace, covariant derivative,localFrameCoeff);Relation/EqvGenuse≤instead ofSubrelation;FunLikecoercion lemmas markedsimp;norm_det/ Bird determinant certification tweaks; small proof cleanups (counterexample, adjoint, cpow deriv, eigenspace closedness).Reviewed by Cursor Bugbot for commit e62f15e. Bugbot is set up for automated code reviews on this repo. Configure here.