Sync upstream mathlib4 (2026-07-29, +26 commits) - #88
Merged
Merged
Conversation
Follow-up to #41507 Generated by Claude Opus, then reviewed and cherry-picked line-by-line by myself. Assisted-by: Claude Opus 4.8
…e mem_minimalPrimes_of_height_le (#42088) According to the theorem statement and docstring, `Ideal.mem_minimalPrimes_of_height_eq` introduced in #21041 should be named `Ideal.mem_minimalPrimes_of_height_le`. This PR renames it accordingly. Co-authored-by: acmepjz <acme_pjz@hotmail.com> Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
…forward instance (#41753) This was one of the slowest declarations to typecheck in mathlib. Replacing an `Iso.refl` with something more explicit yields something which the kernel finds far easier to swallow. As a bonus we can remove a `set_option backward.isDefEq.respectTransparency false`.
…ngs (#42175) In light of #41694, we can remove `FractionRing` from `Module.firank` in `RingTheory/Ideal/Norm/RelNorm.lean`. Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
In this PR we introduce a decomposition of a tensor product of modules induced by a decomposition of the module on the left side. This is used to produce the canonical "energy" grading on a loop Lie algebra. This will (eventually) give us the "energy" grading on smooth representations of affine algebras. Co-authored-by: Oliver Nash <github@olivernash.org>
…#38908) Adds API lemmas extracted from #38813 to keep that PR reviewable: `DirectSum.of_eq_of_eq`, `DirectSum.of_eq_sub_add_smul`, `ModularForm.cast_apply`, `ModularForm.mul_ne_zero`, `ModularForm.sub_smul_isCuspForm`.
…ion (#39161) Thanks to ChatGPT and Gemini for converting part of Yi-Jia Tan's paper into LaTeX, which served as solutions provided to Aristotle. - [x] depends on: #40875 Co-authored-by: Aristotle (Harmonic) <aristotle-harmonic@harmonic.fun> Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> Co-authored-by: Oliver Nash <github@olivernash.org>
All these changes fix issues of the form "A function is expecting `Set α` but is given `α → Prop`, or vice-versa". Generated by Claude Opus, then reviewed and cherry-picked line-by-line by myself. Assisted-by: Claude Opus 4.8
In this PR, we proved `Hom_S (M \tensor S, N \tensor S)` is base change of `Hom_R (M, N)` with respect to `LinearMap.baseChangeHom`. Co-authored-by: Wang Jingting <wangjt2020@163.com> Co-authored-by: Johan Commelin <johan@commelin.net>
…_monomials, eq_monomial_of_unique_weight (#38909) API on MvPolynomials split off from the level-1 modular forms graded ring project (#38813) to keep that PR reviewable. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…f degree divides n (#39239) Co-authored-by: Oliver Nash <github@olivernash.org>
Teaching tactic: `assume p` is short for `intro (_ : p)`. Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
Adds `spectrum.resolvent_sub_resolvent`: For `a b : A` in an `R`-algebra and `r` in the resolvent set of both, `resolvent a r - resolvent b r = resolvent a r * (a - b) * resolvent b r`. Companion to `spectrum.resolvent_eq`.
... and syntactically generalise `{I : Finset ι}` to `{I : Set ι} (hI : I.Finite)`. The new proofs also happen to not abuse the `Set α := α → Prop` defeq.
This pr adds the functionality to transfer Lie brackets along equivalences (additive, linear and plain ones). I followed the scheme of the existing `TransferInstance.lean` file. For one of the proofs, I also needed `linearEquiv_apply `, which seemed missing so I added it. AI use disclaimer: I used claude to search for lemmas/ understand error messages / proofreading and feedback, but wrote the whole code myself.
The old proof abuses defeq in a subtle way, which makes painful reading for the kernel. This one is easier to swallow.
… (#41707) `cache get` downloads files in multiple rounds (corresponding to azure containers, e.g. `master` then `forks` for a fork PR) and decompresses them in a pipeline while the download streams. Each round started from a fresh pipeline state and the round loop kept only the last round's state, so some files queued for decompression plus the in-flight leantar batch was dropped: the .ltars were on disk but never unpacked, and the next lake build recompiled those modules. The in-flight leantar was also never awaited, so it could still be writing build outputs while lake build read them. Reported in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/cache.20issues/with/609923362 The fix makes the pipeline state an explicit value threaded through the rounds: a DecompState structure (pending files, in-flight batch, counters) embedded in TransferState, and finalizeDecomp drain after the last round. Also adds related tests in Cache/Test.lean.
…eclaration (#41883)
Project started during the May 2026 workshop "Techniques and Tools for the Formalization of Analysis" at ICERM. Co-authored-by: Jon Bannon <jbannon@siena.edu> Co-authored-by: Yongxi (Aaron) Lin <aaronlin@andrew.cmu.edu> Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: Oliver Nash <github@olivernash.org> Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr> Co-authored-by: Oliver Nash <github@olivernash.org> Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>
They should not be instance reducible (their entire raison d'être is to be a type synonym to disambiguate typeclass synthesis), but they can be implicit_reducible just fine. This allows removing another 10-20 backcompat options.
…group homs `G → H` (#41995) ... for abelian groups `G` and `H`. Furthermore, the convolution product on bialgebra homs corresponds to pointwise addition on group homs. Also generate more lemmas through `to_additive`, remove some unused `set_option`s and relocate `MonoidAlgebra.toAdditive`/`AddMonoidAlgebra.toMultiplicative` to existing sections. From Toric
In the review of #42173, it was asked if the `have` in `Matrix.ker_diagonal_toLin'` could be removed. This PR does so, and is a bit faster.
This complements the existing `isOpen_Ioo`. Co-authored-by: NoahW314 <noahwalker3.14@gmail.com>
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.12ab8e82f8447fa639dabe9ffeda74436b72be31Auto-merges to
masteronceCI (self-hosted)passes. Regenerateddaily until merged or until a conflict appears.
Note
Low Risk
Routine upstream library sync with no auth or deployment changes; the only behavioral delta in this fork is cache download/decompression plumbing, which is covered by new unit tests.
Overview
Automated merge of 26 commits from
leanprover-community/mathlib4@master.Cache CLI refactors multi-container
cache getdecompression into a dedicatedDecompStatenested underTransferState, threads that state across download rounds viamonitorCurl/downloadFilesFromContainer, and drains it with newfinalizeDecompafter the last round. Download failures are accumulated across rounds instead of only counting the last one.Cache/Test.leanadds unit tests forfinalizeDecompand decompression-state carry.New Mathlib modules (wired in
Mathlib.lean):Analysis.Normed.Operator.Fredholm.Basic(Fredholm operators, packages, TFAE),Algebra.Lie.TransferInstance,LinearAlgebra.Matrix.Nonsingular(semiring nonsingularity vs linear independence), plus graded/tensor decomposition on loop algebras andModule.FinitePresentation.isBaseChange_map.Monoid/group algebras:
RingTheory/Bialgebra/MonoidAlgebra.leangrows substantially—group-like elements,mapDomainBialgHomEquivbetween group homs and bialgebra homs over domains, convolution/lift equivalences, and related API.Broader Mathlib churn: spectrum second resolvent identity;
Irreducible.natDegree_dvd_iff; idealmem_minimalPrimes_of_height_le;relNorm_algebraMapusesfinrank R S; filters/closures use explicit set comprehensions{x | …}; deprecations and proof fixes across manifolds, measure theory, and linear algebra.Reviewed by Cursor Bugbot for commit 773eb14. Bugbot is set up for automated code reviews on this repo. Configure here.