…o separate file (#27337)

This PR moves material that uses `MonoidWithZero` into a separate file.

…o separate file (leanprover-community#27337)

This PR moves material that uses `MonoidWithZero` into a separate file.

…o separate file (leanprover-community#27337)

This PR moves material that uses `MonoidWithZero` into a separate file.

* chore(Algebra/Order/Hom/Monoid): separate MonoidWithZero material into separate file (#27337)

This PR moves material that uses `MonoidWithZero` into a separate file.

* chore(Algebra/Category/MonCat/Basic): fix typos (#27397)

* feat(MetricSpace): tag `dist_nonneg` with `@[simp]` (#27285)

`dist_pos` is already a simp lemma, so `dist_nonneg` should be too.

* chore: add defeq test for grind rings (#26806)

This PR adds a defeq test for multiple paths that convert rings in Mathlib's algebraic hierarchy to abelian groups in grind's hierarchy.
This defeq test used to fail before `leanprover/lean4:v4.22.0-rc3`.

* chore: make create-adapation-pr.sh robust to running on nightly-testing fork (#27411)

cf recent failures at [#nightly-testing > Mathlib bump branch reminders @ 💬](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/Mathlib.20bump.20branch.20reminders/near/530460702)

* chore: bump toolchain to v4.22.0-rc4 (#27415)

* feat(AlgebraicTopology/ModelCategory): a trick by Joyal (#26169)

In order to construct a model category, we may sometimes have basically proven all the axioms with the exception of the left lifting property of cofibrations with respect to trivial fibrations. A trick by Joyal allows to obtain this lifting property under suitable assumptions, namely that cofibrations are stable under composition and cobase change. (The dual statement is also formalized.)

This will be used in the formalization of the model category structure on topological spaces, simplicial sets, simplicial presheaves, etc.



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

* feat(AlgebraicGeometry): codescent implies descent (#23547)

Let `P` and `P'` be morphism properties of schemes. We show some results to deduce
that `P` descends along `P'` from a codescent property of ring homomorphisms.



Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com>

* chore(*): fix some scattered adaptation notes (#27396)

This PR deals with adaptation notes in Mathlib that have become irrelevant or easily fixable. The remainder are going to require actual thinking to fix.

* feat(RepresentationTheory/Homological/GroupHomology): long exact sequences (#25943)

Given a commutative ring `k` and a group `G`, this PR shows that a short exact sequence of `k`-linear `G`-representations 
`0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0` induces a short exact sequence of complexes
`0 ⟶ inhomogeneousChains X₁ ⟶ inhomogeneousChains X₂ ⟶ inhomogeneousChains X₃ ⟶ 0`.

Since the homology of `inhomogeneousChains Xᵢ` is the group homology of `Xᵢ`, this allows us to specialize API about long exact sequences to group homology.



Co-authored-by: 101damnations <101damnations@github.com>

* chore: split `Data.Sign` (#27232)

We now have a `Defs` file defining `SignType` and basic instances, as well as a `Basic` file proving results about the sign function on a ring.

The files have not been changed beyond updating the module description.

* feat(Topology/Algebra/Module/Multilinear/Basic): add simple lemma about `mkPiAlgebra` (#27352)

Also swap the order of some lemmas to put the ones with weaker typeclass assumptions first.

* chore(Analysis): remove a few unneccessary assignments in instance declarations (#27389)

These were introduced mostly as an adaptation for lean4#7717, but they seem to be unnecessary anymore. Since the changes were applied long ago, I can't see the build errors in the logs to figure out the exact issue. (I assume that they simply were not getting inferred.)

In addition to the now-unnecessary `norm_mul_self_le` field for `CStarAlgebra` introduced in those adaptation notes, we can also get rid of quite a few unnecessary `mul_comm` fields.

* fix: delete a duplicate instance (#27402)

This was copied in #27386 to

https://github.com/leanprover-community/mathlib4/blob/d3c295b45d6f0bdb356f99ebe071016f2559eb73/Mathlib/Algebra/GroupWithZero/Action/Hom.lean#L19-L24

but I forgot to delete the original.

* feat(CategoryTheory/Limits): removed possibly faulty simp theorem (#27421)

As discussed [here](https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/.E2.9C.94.20Maximum.20recursion.20error.20at.20simp.20tactic/with/530502013), I got an infinite simp loop where it repeatedly tried to apply `PullbackCone.π_app_left`. This was the definition from mathlib:

```
/-- The first projection of a pullback cone. -/
abbrev fst (t : PullbackCone f g) : t.pt ⟶ X :=
  t.π.app WalkingCospan.left
...
@[simp]
theorem π_app_left (c : PullbackCone f g) : c.π.app WalkingCospan.left = c.fst := rfl
```

Seems like it unfolded the abbrev to immedeately apply the theorem again. So I removed the simp tags, let's see if the build runs through.

* fix: make `CompleteLattice` extend `BoundedOrder` (#26626)

Currently, `CompleteLattice` extends `Top` and `Bot`, and introduces `le_top` and `bot_le`. Finally, `CompleteLattice` introduces an instance of `BoundedOrder`. This PR makes `CompleteLattice` extend `BoundedOrder` directly instead.

* feat(Data/Real): add embedding of archimedean groups into Real (#26114)

This is part of https://github.com/leanprover-community/mathlib4/pull/25140, and is the special case of Hahn embedding theorem applied to archimedean group.

* feat(Abelianization): `lift_symm_apply` (#27423)

Adds a `@[simp]` theorem `lift_symm_apply` and a regular theorem `coe_lift_symm`.

* feat: a monoid algebra is free (#27141)

From Toric

* chore: move `DiscreteUniformity` lower in the import tree (#27384)

* chore: generalize typeclass assumptions on DFinsupp SMul (#27409)

These match the Finsupp instances more closely.

* docs(Simproc/Divisors): fix module docstring (#27420)

Fix the module docstring to reflect the actual names of the dsimprocs

* feat(Polynomial/Algebra): aeval_sub/neg (#27425)

Add lemmas about `sub`/`neg` for `aeval`. These are already available for `eval` and `eval₂`.

* chore(LinearAlgebra/RootSystem): golf `exists_apply_eq_or` and remove note "we should have a tactic to crush this" (#27372)

Remove:

```
  /- The below proof (due to Mario Carneiro, Johan Commelin, Bhavik Mehta, Jingting Wang) should
     not really be necessary: we should have a tactic to crush this. -/
```

We now have such a tactic! 🎉

* chore: rename `Basis` to `Module.Basis` (#27381)

Many other things can have bases.

* feat(RingTheory/Valuation/RankOne): rank one iff value group is mularchimedean (#27436)

Thanks to the ongoing effort to get the Hahn Embedding theorem into Mathlib

* feat(Data/List/DropRight): add reverse and append lemmas  (#27360)

Adds lemmas for rdropWhile and rtakeWhile.

These lemmas were identified while doing work for Project Numina.




Co-authored-by: Bolton Bailey <bolton.bailey@gmail.com>

* fix(to_additive): expand kernel projections to use `reorder` (#27405)

This bug in the `reorder` feature was found while developing `to_dual`. To fix it, we modify the `expand` function to not just eta-expand, but also to expand raw projections.

* feat(Order/DenselyOrderedLocallyFinite): linear locally finite dense orders are trivial (#27172)



Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>

* feat (Algebra/Group/Action/Units): add Units.smul_eq_mul (#27338)

The usual `smul_eq_mul` simp lemma runs into a diamond from two `SMul` instances on units of a `CommMonoid`: `Units.mulAction'.toSMul` and `Mul.toSMul`. This PR adds an extra simp lemma to cover this case.

* chore: unnecessary explicit arguments (#27438)

* feat(Analysis): Spectral norm is nontrivial (#27448)

*From the 2025 Local Class Field Theory Workshop.*

* fix: make `compile_inductive%` work correctly with new compiler (#27401)

The implementation of `compile_inductive%` made assumptions about the implementation of the old compiler that are no longer true. In particular, it looked for compiler IR decls in the kernel env, but these now exist in a private environment extension.

The main use of this check is to avoid recompiling a `sizeOf` definition multiple times within its originating module, so to fix this we just disable the recursive recompilation of inductives within the module of their definition. This means that they will require explicit `compile_inductive%` directives themselves, which were already being supplied anyways.

Fixes #27017.

* chore: remove unnecessary uses of `compile_def%` (#27440)

These were a workaround for bugs in the old compiler (https://github.com/leanprover/lean4/issues/2096) and are no longer necessary.

* doc(to_additive): add comment about overwriting `reorder` (#27388)

It is possible to tag a declaration with `to_additive (reorder := ..)` even when it had already been tagged `to_additive`. This is required for some structure projections like `HPow.hPow`.

* feat(UniformSpace/Ultra/Constructions): IsUltraUniformity.{bot,top} (#27454)

Port of #24412.

* feat(Topology/ClusterPt): Swapped version of `ClusterPt.frequently` (#27407)

This PR adds the theorem
```
theorem ClusterPt.frequently' {F : Filter X} {p : X → Prop} (hx : ClusterPt x F)
    (hp : ∀ᶠ y in F, p y) : ∃ᶠ y in nhds x, p y := by
```
which is basically a swapped version of the existing theorem
```
theorem ClusterPt.frequently {F : Filter X} {p : X → Prop} (hx : ClusterPt x F)
    (hp : ∀ᶠ y in 𝓝 x, p y) : ∃ᶠ y in F, p y :=
```
I'm not sure if there's a common generalization.

* feat(LinearAlgebra/TensorProduct): `map f₂ g₂ (map f₁ g₁ x) = map (f₂ ∘ₗ f₁) (g₂ ∘ₗ g₁) x` (#27142)

From Toric

* feat(RingTheory/SimpleModule): a module over a semisimple ring is both injective and projective (#27154)

Prove that a module over a semisimple ring is both injective and projective. For the injectivity, this follows immediately from `IsSemisimpleModule.extension_property`. For the projectivity, we add a dual statement  `IsSemisimpleModule.lifting_property` to `RingTheory.SimpleModule.Basic`. The actual `Module.Injective` and `Module.Projective` statements are in a separate file `RingTheory.SimpleModule.InjectiveProjective` to minimize imports in `RingTheory.SimpleModule.Basic`.



Co-authored-by: smorel394 <67864981+smorel394@users.noreply.github.com>

* fix: merge master to nightly workflow (#27466)

* feat: `covarianceBilin` lemmas (#27192)

Co-authored-by: Etienne Marion @EtienneC30

From the Brownian motion project.

* feat(Probability): 2 processes have same law iff same finite dimensional laws (#27127)

Co-authored-by: Jonas Bayer @TBUGTB 

From the Brownian motion project.

* feat(Topology/Constructions): add missing instance `CompactSpace (Multiplicative X)` etc (#27463)

* feat: summability results (#27123)

- If a real function is summable, then its sum in ENNReal is finite.
- For a real function `f` with `i <= f i` and `c < 0`, `Summable fun i ↦ exp (c * f i)`

* refactor(SetTheory/Ordinal/Arithmetic): redefine `Ordinal.IsNormal` as `Order.IsNormal` (#26900)

This is of course in anticipation to a subsequent PR that will deprecate `Ordinal.IsNormal` entirely.

- [x] depends on: #26903

* refactor: lemma expressing `ContinuousAt` using a punctured neighbourhood (#25600)



Co-authored-by: Miyahara Kō <52843868+Komyyy@users.noreply.github.com>

* chore: fix indentation of subsequent declaration lines (#27478)

Found by the linter in #27473; not exhaustive.

* feat(CategoryTheory/Monoidal/Opposites): monoid objects internal to the monoidal opposite (#25854)

We construct an equivalence between monoid objects internal to a monoidal category `C`, and monoid objects internal to its monoidal opposite `Cᴹᵒᵖ`. This is done by adding `Mon_Class` and `IsMon_Hom` instance to the relevant objects, as well as by recording an explicit equivalence of categories `Mon_ C ≌ Mon_ Cᴹᵒᵖ`.



Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>

* feat(Data/Nat/Digits): mod b^n is equivalent to taking first n digits in base b (#27354)

This PR adds `mod` and `take` lemmas analogous to the existing `div` and `drop` lemmas, [ofDigits_div_pow_eq_ofDigits_drop](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Digits/Defs.html#Nat.ofDigits_div_pow_eq_ofDigits_drop) and [self_div_pow_eq_ofDigits_drop](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Digits/Defs.html#Nat.self_div_pow_eq_ofDigits_drop).

* chore: fix more indentation (#27491)

Found by the linter in #27473.

* feat(Logic/Embedding/Basic): simp lemmata for arrowCongrLeft (#27345)

This PR adds some basic facts about `arrowCongrLeft`. They seem to be useful when manipulating formal series in multiple variables.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

* chore: fix more indentation (#27494)

Found by the linter in #27473.

* feat: `norm_num` extensions for Ordinals (#27343)



Co-authored-by: Miyahara Kō <52843868+Komyyy@users.noreply.github.com>

* feat(Analysis/InnerProductSpace/Adjoint): an operator `T` is normal iff `‖T v‖ = ‖(adjoint T) v‖` (#27476)

* fix(Data/NNReal): type-correct `GroupWithZero` instance on `NNReal` (#27483)

We can get a `GroupWithZero` instance on `NNReal` via the `Semifield` instance or via the `LinearOrderedCommGroupWithZero` instance. Under reducible-with-instances these are defeq, but in the process we non-reducibly-with-instances unfold `NNReal` to `{x // 0 ≤ x}`. To correct this mismatch, we either need to redefine the instances on `NNReal` to respect this non-reducibility, or we can make sure the unification succeeds without unfolding `NNReal`. The latter seems to give fewer headaches.

(In the long run, are we going to unbundle `LinearOrderedCommGroupWithZero` like we did for the other ordered algebra objects?)

This issue was spotted because `gcongr` didn't work reliably on `NNReal` anymore; see the fixed adaptation notes.

* chore(Analytic/Linear): replace a ContinuousLinearMap with a ContinuousLinearEquiv (#27477)

`ContinuousLinearEquiv.analyticWithinAt` and `ContinuousLinearEquiv.analyticOn` took a `ContinuousLinearMap` argument. This PR fixes that.

* feat(Data/Matrix): matrices with entries in a set (#27190)

Define the `Set`/`AddSubmonoid`/`AddSubgroup`/`Subring`/`Submodule`/`Subalgebra` of matrices with entries in a `Set`/`AddSubmonoid`/`AddSubgroup`/`Subring`/`Submodule`/`Subalgebra`. 

[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Set.2Ematrix/near/527826651)

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>



Co-authored-by: bwangpj <70694994+bwangpj@users.noreply.github.com>
Co-authored-by: Bryan Wang Peng Jun <70694994+bwangpj@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

* feat: mark `HasFiniteIntegral` with `fun_prop` (#27506)

And use it to golf a few proofs.

* feat: generalise more lemmas to enorms (#27456)

The selection of lemmas may seem eclectic, but follows a clear path: these are necessary for generalising the last section of IntegrableOn.lean to enorms.

* feat(Analysis): radius of convergence for `FormalMultilinearSeries.compContinuousLinearMap` (#26255)

- Add basic lemmas `compContinuousLinearMap_id` and `compContinuousLinearMap_comp`.  
- Prove lower and upper bounds for the convergence radius of `f.compContinuousLinearMap`.  
- Prove `radius_compNeg`: the convergence radii of `f(x)` and `f(-x)` are equal.

* feat(Probability): covariance of sums and maps (#26998)

Variance and covariance of sums of random variables.
Covariance with respect to the map of a measure.

Co-authored-by: @EtienneC30 

From the Brownian motion project.

* feat: measure_inter_eq_of_ae (#27247)

For a measure `μ` and two sets `s, t`, if `∀ᵐ a ∂μ, a ∈ t` then `μ (t ∩ s) = μ s`.

From the Brownian motion project.

* feat(RingTheory/Valuation/Discrete/Basic): relate DVRs and discrete valuations (#26623)

We prove that the valuation subring of a discretely-valued field is a DVR.

Conversely, given a DVR `A` and a field `K` satisfying  `IsFractionRing A K`, we show that the valuation induced on `K` is discrete.

We provide the ring isomorphism between a DVR and the valuation subring in its field of fractions endowed with the adic valuation of the maximal ideal.

Co-authored-by: @faenuccio 



Co-authored-by: faenuccio <filippo.nuccio@univ-st-etienne.fr>
Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>

* feat(Analysis/CStarAlgebra/...): an idempotent element in a C*-algebra is self-adjoint iff it is normal (#27475)

* feat(Algebra/Star/SelfAdjoint): some API for `IsStarNormal` (#27095)

This adds api for adding and subtracting normal elements.

* chore(Data/List): remove 9 month old deprecations (#27518)

These deprecations were introduced in https://github.com/leanprover-community/mathlib4/commit/a7fc949f1b05c2a01e01c027fd9f480496a1253e, but the year was miswritten as being in the future!

* feat: api for symmetric bilinear forms (#26274)

Change the definition of `BilinForm.IsSymm` to make it a structure, in order to extend it to define `ContinuousBilinForm.IsPosSemidef` in #26315.
Prove polarization identity.
Prove two lemmas about `BilinForm.toMatrix`.



Co-authored-by: EtienneC30 <66847262+EtienneC30@users.noreply.github.com>

* feat: inner product against basisFun (#26378)

Also remove the `simp` attribute off [PiLp.inner_apply](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/InnerProductSpace/PiL2.html#PiLp.inner_apply).

From Brownian Motion



Co-authored-by: EtienneC30 <66847262+EtienneC30@users.noreply.github.com>

* chore: golf `image_support_finSuccEquiv` using `grind` (#27469)

* feat(Data/Set): add `sep_subset_setOf` (#27087)

which is the counterpart of `sep_subset` for use in term mode.



Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

* feat(Algebra/Order/Sub): add `map_tsub_of_le` (#27088)

An `AddHom` keeps ordered subtraction in canonically ordered monoids. This is a simple corollary of `tsub_add_cancel_of_le`.

* feat(Data/List): add theorem `List.nodup_concat` (#27459)

This contribution was created as part of the Utrecht Summerschool "Formalizing Mathematics in Lean" in July 2025.

* feat(Order/Interval/Finset/Nat): `(List.range x).toFinset = Finset.range x` (#27480)

* chore: rename `IsAdjoinRootMonic.Monic` to `IsAdjoinRootMonic.monic` (#27503)

It's a proof, not a prop.

* fix(to_additive): don't consider extra attributes in `to_additive self` (#27474)

When using `to_additive self`, it doesn't make sense to use `(attr := ...)`. Additionally, the `existingAttributeWarning` linter should be disabled.

* feat(MeasureTheory/SimpleFunc): add instances of algebraic structures (#27336)

This adds a `Star` instance on simple functions into a type with a star structure, the associated `coe_star` lemma, and the relevant algebraic compatibility instances (e.g., `StarMul`) when the codomain is equipped with these.

We also add several missing instances (mostly `Ring`-like and `Algebra`-like).

This PR is the first in a series of small PRs aimed at providing a `CStarAlgebra` instance for L^∞ functions.

* docs: typo in `whiskerRight` docstring (#27489)

The docstring for `whiskerRight` accidentally duplicated `G`:

> If `α : G ⟶ H` then `whiskerRight α F : (G ⋙ F) ⟶ (G ⋙ F)` ...

This PR also tweaks the formatting of the docstrings for `whiskerLeft` and `whiskerRight`, which can fit on one line.

* feat(Topology/Instances/Matrix): topology of `Set.matrix` (#27496)

Prove topological results (`IsOpen`, `IsCompact`) about `Set.matrix`. 

- [x] depends on: #27190 

[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Set.2Ematrix/near/527826651)

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>



Co-authored-by: bwangpj <70694994+bwangpj@users.noreply.github.com>
Co-authored-by: Bryan Wang Peng Jun <70694994+bwangpj@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

* chore: more indentation fixes (#27502)

Found by the linter in #27473.

* chore(Algebra/Algebra/Defs): modified `RingHom.toAlgebra'` and `RingHom.toAlgebra` docstrings to reflect the risk of diamonds (#27514)

Modified the docstring of `RingHom.toAlgebra'` to include a warning that if `S` already has a `SMul R S` 
instance, then using this result creates another `SMul R S` instance from the supplied `RingHom` and 
this will likely create a diamond. Also modified `RingHom.toAlgebra` similarly (a bit shorter, since this result calls the primed version, so the warning here says that the call to the primed version may create a diamond.)



Co-authored-by: Jon Bannon <59937998+JonBannon@users.noreply.github.com>

* chore: Clean up typos using OpenAI's GPT-4.1 mini (verified by human) (#27519)

This commit was generated using OpenAI's GPT-4.1 mini and then verified by a human.

A human-written script was run (powered by the aforementioned AI model) on the first 20 files in the `Mathlib/` folder.

* feat: add mdifferentiable analogues of C^n metric lemmas (#26921)

* chore: generalize `sumAddHom` to `sumZeroHom` (#27272)

This hopefully will make this usable on quadratic maps, which preserve zero but not addition.

For now this does not change the simp-normal form of `sumAddHom`

* docs: Inherit `Equivalence` docstring on notation (#27487)

The prior docstring for the notation `≌` for `Equivalence` read only

> We infix the usual notation for an equivalence

This PR instead attaches `@[inherit_doc Equivalence]` to the notation, so that information for `Equivalence` is displayed when hovering over `≌`.

We also clean up the formatting and grammar of the docstrings for `Equivalence` and its fields, and make them less "context-specific" (and therefore more appropriate for hovers) without changing their content radically.

* feat: `apply` and `coe` results for `UniformSpace.Completion.mapRingHom` (#24872)

* chore: rename Analysis.Meromorphic.Gamma to Analysis.Meromorphic.Complex (#27499)

This PR renames Analysis.Meromorphic.Gamma to Analysis.Meromorphic.Complex since additional meromorphicity results will be added in #27500.

* chore(Algebra/Category/ModuleCat): remove use of `erw` in `coconeMorphism` (#27522)

* chore(CategoryTheory/Idempotents): remove use of `erw` in `split_iff_of_iso` (#27523)

* chore: chore(Order): use new ge/gt - Part 6 (#27528)

This PR fixes 2 more order names: `forall_ge_iff_le` now aligns with `le_of_forall_ge`. And I think I made an error when applying the new naming convention for `eq_or_lt_of_not_gt`.

* chore: remove a few superfluous open's (#27488)

Found by the linter in #25362.

* feat(ZMod): add `to_additive_dont_translate` (#27521)

This PR adds the tag `@[to_additive_dont_translate]` to `ZMod`, so that it is treated the same as `ℕ` by `to_additive`. This allows us to use `to_additive` in 2 more places.

* feat(Algebra/Order): additional lemma about mkRat pos/neg (#27501)

There is `mkRat_nonneg` in the same file. This adds iff version for all pos/neg/nonpos/nonneg

* feat: establish examples of harmonic functions (#26844)

If `f : ℂ → F` is complex-differentiable, then show that `f` is harmonic. If `F = ℂ`, then so is its real part, imaginary part, and complex conjugate. If `f` has no zero, then `log ‖f‖` is harmonic.

This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. It is one of the ingredients in the proof of Jensen's Formula in complex analysis.

* chore: replace `Monoid.IsTorsionFree` with `IsMulTorsionFree` (#24311)

From Toric

* feat(AlgebraicGeometry): Add global preorder instance for schemes (#26204)

In this PR we added a default preorder instance for schemes, defined to be the specialization order as discussed here: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/dimension.20function.20for.20schemes/near/524997376 for discussion 



Co-authored-by: Raph-DG <77658801+Raph-DG@users.noreply.github.com>

* feat(CategoryTheory/Monoidal/DayConvolution): braiding and symmetry for Day convolution (#27067)

In this PR, we prove that when `C` and `V` are braided monoidal categories, and when relevant Day convolutions exist, the unbundled Day convolution monoidal structure on `C ⥤ V` is also braided: we construct an isomorphism  `DayConvolution.braiding`, characterize it with respect to the unit maps that exhibits Day convolutions as left Kan extensions, and prove that the forward and reverse hexagon identities are satisfied. 

In the case `C` and `V` are symmetric, we show that `braiding F G|>.hom` is inverse to `braiding G F|>.hom` as well.



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

* feat: `OrderEmbedding` is a topological embedding (#27512)

`OrderEmbedding` is a topological embedding provided that the range of `f` is order-connected.

Co-authored-by: Rémy Degenne <remy.degenne@inria.fr>



Co-authored-by: Gaëtan Serré <56162277+gaetanserre@users.noreply.github.com>

* chore(CategoryTheory/Localization): remove use of `erw` in `homMap_map` (#27524)

* fix: fetch depth for master to nightly workflow (#27533)

Fixes the fetch depth for the "Merge master to nightly" workflow; we need to have the entire commit history or else we'll have weird unwanted side effects.

* chore: update Mathlib dependencies 2025-07-27 (#27530)

This PR updates the Mathlib dependencies.

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Kim Morrison <kim@tqft.net>

* chore: Clean up typos using OpenAI's GPT-4.1 mini (verified by human) (#27535)

This commit was generated using OpenAI's GPT-4.1 mini and then verified by a human.

A human-written script was run (powered by the aforementioned AI model) on the files № 101-200 in the `Mathlib/` folder.

* feat: `small_plift` (#27541)

Adds an instance `small_plift`.

* chore(Analysis/InnerProductAlgebra/Projection): adding norm and other results for `Submodule.starProjection` (#27317)

Analogue results for `Submodule.starProjection`.

* feat: implement the Cauchy-Riemann Equation (#26839)

Describe complex differentiability for functions `f : ℂ → ℂ` using the Cauchy-Riemann equation.

This material closes a long-standing open TODO. It is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. It is one of the ingredients in the proof of Jensen's Formula in complex analysis.

* chore: golf Ideal.span_singleton_mul_left_unit (#27543)

* feat(LinearAlgebra/Projection): lemmas on projections and invariant submodules (#25874)

Proving some lemmas on invariant submodules, such as:

For idempotent `f` and any operator `T`:
- `range f` is invariant under `T` iff `f ∘ T ∘ f = T ∘ f`
- `ker f` is invariant under `T` iff `f ∘ T ∘ f = f ∘ T`
- `f` and `T` commute iff both `range f` and `ker f` are invariant under `T`

Added for both linear maps and continuous linear maps for convenience.

Taken from leanprover-community/mathlib3#18289.



Co-authored-by: Monica Omar <2497250a@research.gla.ac.uk>

* style: use simplex notation (`⦋n⦌`) where possible (#25322)

`StandardSimplex.mk n` is replaced with `⦋n⦌` where possible (except in notation and macros, which are left untouched). This includes opening `Simplicial` (`scoped`) in two files. Also, outdated and unused `local notation` `[n]` for `StandardSimplex.mk n` is removed.



Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

* chore(Analysis/InnerProductSpace/GramSchmidtOrtho): change definition to use `U.starProjection x` instead of `(U.orthogonalProjection x : E)` (#27334)




Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>

* feat(Data/Rat): add lemma for multiplying num or den (#27495)

Small lemmas for Rat split off from #26059. These restates `mul_num` and `mul_den` so one doesn't need to deal with integer division.

* feat: describe posLog in terms of circle averages (#27160)

If `a` is any complex number of norm one, establish by direct computation that the circle average `circleAverage (log ‖· - a‖) 0 1` vanishes.

As soon as the mean value theorem for harmonic functions becomes available, this result will be extended to arbitrary complex numbers `a`, showing that the circle average equals the positive part of the logarithm, `circleAverage (log ‖· - a‖) 0 1 = log⁺ ‖a‖`. This result, in turn, is a major ingredient in the proof of Jensen's formula in complex analysis.

* chore(Analysis/InnerProductSpace/Projection): change `_of_completeSpace` to `_of_hasOrthogonalProjection` (#27559)

This PR renames the results because they use `Submodule.HasOrthogonalProjection` and not `CompleteSpace`.

* feat: `small_quot` and `small_quotient` (#27546)

Adds instances for small quotients.

* feat(Nat/ModEq): `a - c ≡ b - d` if `a ≡ b` and `c ≡ d` (#27568)

* feat(Analysis/InnerProductSpace/Adjoint): a normal idempotent operator is a star projection (#26767)

This adds that an idempotent operator is self-adjoint if and only if it is normal. This means that a normal idempotent operator is a star projection.

Along with #26631, we get that for idempotent operators, normality, self-adjointedness, and positivity are all equivalent.



Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>

* refactor(Analysis/InnerProductSpace/Positive): changing positivity on linear maps to use `IsSymmetric` instead of `IsSelfAdjoint` and finite-dimensionality (#27089)

With this definition, the partial order would be defined on linear maps without needing finite-dimensionality.

Also, when continuous linear maps are positive, then so are their coercions into linear maps, again, without needing finite-dimensionality. Moving the definition of positivity for linear maps before the one for continuous linear maps allows us to use results already done in linear maps for continuous linear maps. There's no need to have duplicate proofs.

In essenece:
- This changes the definition of `LinearMap.IsPositive` to `IsSymmetric T` instead of `IsSelfAdjoint T` and removes the finite-dimensional hypothesis.
- This changes the order of the whole file: starting with linear maps and ending with continuous linear maps, instead of the other way around.
- Adds `LinearMap.IsSymmetric.natCast`.
- Adds `LinearMap.IsIdempotentElem.isPositive_iff_isSymmetric`, which is then used to golf `ContinuousLinearMap.IsIdempotentElem.isPositive_iff_isSelfAdjoint` (note the change of order for `isPositive_iff_isSelfAdjoint` and `IsPositive.of_isStarProjection`).
- Final addition: `ContinuousLinearMap.coe_le_coe_iff` which just says `f.toLinearMap ≤ g.toLinearMap` iff `f ≤ g`.
- There are two results (`LinearMap.IsPositive.conj_adjoint` and `LinearMap.IsPositive.adjoint_conj`) which are in the middle of the `ContinuousLinearMap` namespace. The reason for this is to utilize the proofs already done for continuous maps instead of having duplicate proofs.



Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>

* chore: specify merge behaviour in create-adaptation-pr.sh (#27571)

See previous failure at https://github.com/leanprover-community/mathlib4-nightly-testing/actions/runs/16556890710/job/46819596244#step:17:63

* chore(RepresentationTheory/Rep): remove use of `erw` in `counitIso` (#27555)

* feat: `⋃ x ∈ s ×ˢ t, f x.1 ×ˢ g x.2 = (⋃ x ∈ s, f x) ×ˢ (⋃ x ∈ t, g x)` etc. (#27016)

This lemma is needed to prove that finite product of Alexandrov-discrete spaces is Alexandrov-discrete: #27018 

This is the generalization of [Set.iUnion_prod](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Lattice/Image.html#Set.iUnion_prod) to `biUnion`.

Also generalize pi version.

Also generalize the type of the lemma
```lean
`⋃ (i : ι), ⋃ j, ⋃ (i' : ι), ⋃ j', s i j i' j' = ⋃ (i' : ι), ⋃ j', ⋃ (i : ι), ⋃ j, s i j i' j'`
```
to
```lean
`⋃ (i : ι), ⋃ j, ⋃ (i' : ι'), ⋃ j', s i j i' j' = ⋃ (i' : ι'), ⋃ j', ⋃ (i : ι), ⋃ j, s i j i' j'`
```

* chore(CategoryTheory/Monoidal): unify `mkIso` (#27126)

Previously, `mkIso` and `mkIso'` meant different things across the various types of objects. Now:
* `mkIso'` takes in elements `X`, `Y` of the underlying category `C`, an isomorphism `e : X ≅ Y` and a typeclass assumption `[IsMon_Hom e.hom]` and returns `mk X ≅ mk Y`,
* `mkIso` is an `abbrev` for `mkIso'`, taking in elements `X`, `Y` of  `Obj C`, an isomorphism `e : X.X ≅ Y.X` and the proof fields of `IsMon_Hom e.hom` and returns `X ≅ Y`.

From Toric

* feat(MeasureTheory/Measure/AddContent): Add lemma `addContent_biUnion_eq` (#27406)

This PR adds a lemma `addContent_biUnion_eq` stating than an `AddContent` is additive on a finite pairwise disjoint union. We already have the inequality `addContent_biUnion_le` without the pairwise disjoint assumption.

* feat(SetTheory/ZFC/VonNeumann): von Neumann hierarchy of sets (#26543)

Ported from #17027. For extra discussion on this PR, see [Zulip](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2317027.20.2C.20.2326518.20von.20Neumann.20hierarchy/with/526389347).

* feat(Mathlib/MeasureTheory/MeasurableSpace/Invariants): add `comp_eq_of_measurable_invariants` (#26853)

Invariance of `g` follows from `Measurable[invariants f] g`.

Co-authored-by: Lua Viana Reis <me@lua.blog.br>




Co-authored-by: Oliver Butterley <51876429+oliver-butterley@users.noreply.github.com>

* chore(LinearAlgebra/Matrix/Ideal): deprecate `matricesOver` (#27575)

`Ideal.matricesOver` is not an ideal name - one should use `matrix` instead of `matricesOver`, see also #27190 where the analogous `Set.matrix`, `Subring.matrix`, etc are defined. 

[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Set.2Ematrix/near/527826651)



Co-authored-by: bwangpj <70694994+bwangpj@users.noreply.github.com>

* feat(Probability): Prove Hoeffding's lemma corollary  (#27230)

Prove a corollary of Hoeffding's lemma for random variables with non-zero expectation.

This simple corollary was suggested by a reviewer based on a recent contribution  (#26744).

* feat(Analysis/Analytic): `HasFPowerSeriesOnBall.compContinuousLinearMap` (#26268)

Prove `HasFPowerSeriesOnBall.compContinuousLinearMap` and its variants: if `pf` converges to `f` on the ball `B(u x0, r)` where `u` is continuous linear function, then `pf.compContinuousLinearMap u` converges to `f ∘ u` on `B(x0, r / ‖u‖)`.

* chore(LinearAlgebra/QuadraticForm): missing `coe_mk` and `norm_cast` (#27450)

Also fixes an over-applied `simps`.

* chore: scope the instances giving a normed space structure from a Riemannian bundle instance (#27462)

These are costly and quite specific. See discussion at [#mathlib4 > type-class inference slow/timing out @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/type-class.20inference.20slow.2Ftiming.20out/near/530312318)

* feat: add lemmas for modular exponentiation with the totient function (#26694)

This PR adds lemmas around reducing the exponent of a modular exponentiation.

These lemmas were found while doing work for [Project Numina](https://projectnumina.ai/).



Co-authored-by: Bolton Bailey <bolton.bailey@gmail.com>

* fix(to_additive): expand projections more often (#27529)

This PR is a follow-up on #27405, since that PR didn't actually fix the original problem with the proof generated by `@[reassoc]`.

It turns out that we should always expand projections if they have been explicitly tagged with `@[to_additive]` or `@[to_dual]`. In this case, `CategoryTheory.NatTrans.naturality` is not dual to itself, but its dual is proven separately, and tagged with `@[to_dual existing]`. So, we really need to expand the projection.

There is no clear way to tell if a projection has been tagged explicitly,  or automatically when tagging the structure. So, projections are sometimes expanded unnecessarily.

* feat(AlgebraicGeometry): Any stalk of a locally noetherian scheme is Noetherian (and ditto for integral schemes) (#26850)

In this PR we show any stalk of a locally noetherian scheme is Noetherian (and ditto for integral schemes), and we write these results as typeclass instances.

* chore(to_additive): fix `firstMultiplicativeArg` implementation (#27526)

I didn't find any bad behaviour resulting from this. But the implementation seems to be doing the wrong thing in the case of an application `fn args` where `fn` is not a constant.

(And `List.foldl` is the more efficient fold)

* feat: if `F` is fully faithful, then so is `F.mapGrp` (#27580)

Follow up to #23874. Also remove the corresponding `noncomputable` as they are now unnecessary.

From Toric

* chore: update Mathlib dependencies 2025-07-28 (#27603)

This PR updates the Mathlib dependencies.

* chore: remove useless assumption in measure instances (#27594)

* feat(Analysis/InnerProductSpace/Positive.): add theorem `LinearMap.IsPositive.of_isStarProjection` (#27246)

This two theorems where already added for `ContinuousLinearMap`, and in this pull request I'm adding them for `LinearMap`

* feat(Analysis/VonNeumannAlgebra/Basic): idempotent in von Neumann algebra iff its range and kernel are invariant under commutant (#26799)

This adds that an idempotent operator is in a von Neumann algebra iff its range and kernel are invariant under the commutant.

(This is from leanprover-community/mathlib3/pull/18290.)



Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>

* chore(Analysis/InnerProductSpace/Adjoint): typo in docstring (#27607)

* chore(CategoryTheory/Limits): remove use of `erw` in `Cofork.IsColimit.mk` (#27611)

* chore(CategoryTheory/Limits): remove use of `erw` in `colimitCoconeOfUnique` (#27612)

* feat(LinearAlgebra/Projection): define `Submodule.IsCompl.projection` (#27369)

This defines `Submodule.IsCompl.projection`: the linear projection onto a subspace along its complement as a map from the full space to itself, as opposed to `Submodule.linearProjOfIsCompl`, which maps into the subtype.
This version is important as it satisfies `IsIdempotentElem`.

This is the linear map version of `Submodule.starProjection` when in a complete space where `IsCompl U Uᗮ`.

An operator `T` is idempotent iff it equals the projection onto its range along its kernel (i.e., `Submodule.IsCompl.projection` where `IsCompl (range T) (ker T)`).

An idempotent operator `T` is symmetric if and only if its range and kernel are pairwise orthogonal (a more general `ContinuousLinearMap.IsIdempotentElem.isSelfAdjoint_iff_orthogonal_range` - so proof of this is golfed).

Next pr: deprecate all instances of `p.subtype.comp p.linearProjOfIsCompl q hpq` and `(p.linearProjOfIsCompl q hpq x : E)` to `hpq.projection` and `hpq.projection x` respectively.



Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>

* fix: reword instructions for adding co-authors in the PR template (#27618)

This remedies the issue reported in the associated Zulip topic, namely, that the merge commit squashed by bors includes the co-authors who did not author commits in a way that is not recognized by GitHub.

https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/co-authored-by.20bors.20issue/with/531479378

* chore(Algebra/Quotient): fix deprecated links (#27593)

* feat(Fin2): equiv with `Fin` (#27595)

* chore(FieldTheory/IntermediateField): remove use of `erw` in `adjoin_minpoly_coeff_of_exists_primitive_element` (#27613)

* chore(LinearAlgebra/Dimension): remove use of `erw` in `lift_rank_eq_of_equiv_equiv` (#27614)

* chore(Topology/Gluing): remove use of `erw` in `eqvGen_of_π_eq` (#27617)

* chore(LinearAlgebra/PiTensorProduct): remove use of `erw` in `reindex_refl` (#27553)

* feat(Linter/TextBased): linter against Windows-forbidden filenames (#27588)

[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Never.20name.20a.20file.20Con.2Elean/with/531323255)




Co-authored-by: grunweg <rothgang@math.uni-bonn.de>

* chore: some whitespace fixes (#27485)

Found by the linter in #26926.

* chore: add space around `rintro`/`rcases`/`obtain` or-patterns (#27486)

The pretty-printer enforces spaces in or-patterns, e.g. `_|_|x` to `_ | _ | x` (which seems clearly good).
I'm on the fence about `(_|_)`

* feat(CategoryTheory/Monoidal: an isomorphism of group objects is an isomorphism of the underlying objects (#27137)

From Toric

* feat(Algebra/Order): Locally Finite Linearly Ordered Abelian Groups (#27430)

We prove that `ℤ` is the only Locally Finite Linearly Ordered Abelian Group.

We also move `OrderMonoidIso.toAdditive` and friends from `Mathlib/GroupTheory/ArchimedeanDensely.lean` to a new file.



Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

* feat(Composition): tag simp lemmas (#27458)

Add two simp lemmas `embedding_comp_inv` and `index_embedding`.

* chore: create-adaptation-pr.sh is more careful about remotes (#27621)

* fix(KaehlerDifferential): avoid brackets around `Ω[S⁄R]` notation (#27601)

There is no reason to need the brackets around `Ω[S⁄R]`. This PR fixes the notation.

* chore(Probability/Process): golf entire `hitting_of_lt` using `grind` (#27616)

* feat (Mathlib/Dynamics/BirkhoffSum/Basic): add lemma `birkhoffSum_of_comp_eq` (#26810)

If a function `φ` is invariant under a function `f` (i.e., `φ ∘ f = φ`), then the Birkhoff sum of `φ` over `f` for `n` iterations is equal to `n • φ`.

Co-authored-by: Lua Viana Reis <me@lua.blog.br>



Co-authored-by: Oliver Butterley <51876429+oliver-butterley@users.noreply.github.com>
Co-authored-by: Lua 🌒 <me@lua.blog.br>

* feat: remove (upstreamed) shake (#27632)

`shake` has been moved to Batteries.

* chore: fix scripts to correctly locate bump/ branches on nightly-testing fork (#27572)

See [zulip](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/Mathlib.20bump.20branch.20reminders/near/531241356)[#nightly-testing > Mathlib bump branch reminders @ 💬](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/Mathlib.20bump.20branch.20reminders/near/531241356) discussion.

* chore: make create-adaptation-pr.sh more idempotent (#27623)

* feat(Algebra/Order): `pow_le_pow_iff_right_of_lt_one₀` (#27624)

Add `pow_le_pow_iff_right_of_lt_one₀`. (Analogous to `zpow_le_zpow_iff_right_of_lt_one₀`.)

* chore: move MvPolynomial.algebraMap_apply earlier (#27631)

* chore: generalize Subgroup.mem_mk and related lemmas (#27629)

* chore: add githelper.py script (#26023)

As described in the readme file, this somewhat opinionated script aims to help fix weird git repo setups and restore them to a standardized state that closely matches what `gh repo clone` does. Like `migrate_to_fork.py`, this script requires the user to have `git` and `gh` installed.

To use the script, run `scripts/githelper.py fix` in a git repo that is either a clone of mathlib or of a mathlib fork. The script will prompt you before making any changes, so the user retains control over the entire process. The script also prints the commands used.

`fix` is a subcommand so other git and github management tasks can be added in the future. Possible examples: Deleting branches of closed PRs, keeping the fork in sync with upstream, removing branches from a fork that was accidentally cloned with all mathlib branches included.

* feat: With{Bot,Top}.map_injective (#27651)

Using `Option.map_injective` in downstream code would be defeq abuse.

* chore(Algebra/BigOperators): golf `prod_congr_of_eq_on_inter` using `grind` (#27653)

* refactor: Rename ContinuousLinearMap.toLinearMap₂ (#27574)

Rename `ContinuousLinearMap.toLinearMap₂` to `ContinuousLinearMap.toLinearMap₁₂`.

See the discussion here: https://github.com/leanprover-community/mathlib4/pull/26345#pullrequestreview-3059683061

* feat(combinatorics): Add weight function for Quiver.Path (#27315)

This is part of work toward proving the Perron-Frobenius theorem.

--

This PR introduces a generic weight function for paths in a quiver, where edge weights are elements of a monoid. This is the first in a series of planned contributions to Quiver.Path API, with the ultimate goal of PRing the formalized Perron-Frobenius theorem for primitive and irreducible matrices here .

https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Formalizing.20Perron-Frobenius/with/525516636

The Perron-Frobenius theorem relies on analyzing the powers of a matrix, which correspond to the number (or total weight) of paths of a given length in the graph represented by the matrix, so a robust API for path manipulation is a prerequisite.

This API is built on Quiver because it is fundamentally concerned with the properties of paths as sequences of specific, identifiable arrows (a ⟶ b). The Digraph structure, which models adjacency as a relation, abstracts away the identity of individual edges and would not support the construction and manipulation of paths in the required manner (not in my attempts at least). Similarly, Graph is designed for undirected graphs. Therefore, I think Quiver is the appropriate foundational layer for this work

Main features of this PR are:

It defines Quiver.Path.weight as the monoidal product of weights along a path.
It adds a convenience wrapper Quiver.Path.weight_of_fn for when weights are determined by a function on the vertices.
It proves that weight is a monoid homomorphism (weight_comp).
It includes lemmas establishing that positivity (weight_pos) and non-negativity (weight_of_fn_nonneg) of weights are preserved, which will be crucial for the Perron-Frobenius application.

Subsequent PRs will (partly) build on this by introducing:

- Definitions for the vertices of a path (Path.vertices) and core properties.
- Lemmas for path decomposition and splitting.
- A formalization of simple paths and cycles, including cycle extraction.
- The theorem that a shortest path is always simple.



Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>

* refactor(FieldTheory/Galois): Switch from `Fintype` to `Finite` (#25997)

This PR switches mathlib's Galois theory from `Fintype` to `Finite` to match the group theory library.

* fix(LinearAlgebra/TensorProduct): fix `⊗[R]` precedence (#27590)

This PR makes `⊗[R]` have the same precedence as the infixl `⊗` notation. And it fixes the brackets where necessary.

* chore(Analysis): make argument explicit to `CFC.sqrt_nonneg` and `CFC.sqrt_eq_rpow` (#27684)

These two lemmas had all arguments implicit, which means we have to add implicit argument hints in a few places: `sqrt_nonneg (a := a) : 0 ≤ sqrt a`. For `Real.sqrt_nonneg` and similar, the a argument is explicit. Making it explicit here avoids a few type ascriptions and implicit argument hints.

* feat(LinearAlgebra.DirectSum.Finite): a finite direct sum of finite modules is a finite module (#27092)

Prove that a finite direct sum of finite modules is a finite module.

There are instances both in the `DFinsupp` and `DirectSum` namespaces, to help type class inference find them.




Co-authored-by: smorel394 <67864981+smorel394@users.noreply.github.com>

* feat(MonoidAlgebra): generalize IsDomain instance (#27241)

The instance works over a semiring with cancellative addition. It's then used to generalize the IsDomain instances on Polynomial and MvPolynomial.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

* chore(Nat): change argument from `0 < n` to `n ≠ 0` (#27647)

Style guide says arguments should be in the weaker form

Some proofs got longer because internally they had `0 < n` available or relied on iffs that simplified statements about positive elements

* feat(Analysis/InnerProductSpace/Adjoint): `v` in star projection range iff `‖T v‖ = ‖v‖` (#27619)

* fix(LinearAlgebra/TensorProduct): fix `⊗ₜ[R]` precedence (#27589)

This PR makes `⊗ₜ[R]` have the same precedence as the infixl `⊗ₜ` notation. This also affects the pretty printer, making it consistent with `⊗ₜ`.



Co-authored-by: Jovan Gerbscheid <56355248+JovanGerb@users.noreply.github.com>

* chore: Clean up typos using OpenAI's GPT-4.1 mini (verified by human) (#27539)

This commit was generated using OpenAI's GPT-4.1 mini and then verified by a human.

A human-written script was run (powered by the aforementioned AI model) on the files № 201-300 in the `Mathlib/` folder.

* feat: hook up ordered ring instances for grind (#27620)

* fix: make mathlib4 upstream handling stricter (#27646)

As reported at [#mathlib4 > Feedback on scripts/migrate_to_fork.py @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Feedback.20on.20scripts.2Fmigrate_to_fork.2Epy/near/531482791).

* chore: fix many typos (powered by OpenAI's GPT-4.1 mini) (#27545)

Co-authored by @Rob23oba. Powered by OpenAI's GPT-4.1 mini.

@Rob23oba [wrote a Lean program](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Let's.20catch.20typos!/near/527735131) to find all tokens used in Mathlib's declarations, and [posted a full list](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Let's.20catch.20typos!/near/527737473). Then, I ran OpenAI's aforementioned model on said list, and got a list of about 300 potential typos. Then I replaced them manually using VSCode's editor and used the deprecation script.

Since this is done using a frequency analysis algorithm, naturally it will miss "contextual typos", where the typo is still a valid word but used in the wrong context.

* chore: Clean up typos using OpenAI's GPT-4.1 mini (verified by human) (#27532)

This commit was generated using OpenAI's GPT-4.1 mini and then verified by a human.

A human-written script was run (powered by the aforementioned AI model) on the files № 21-100 in the `Mathlib/` folder.

* chore(Algebra/GeomSum): golf `op_geom_sum₂` using `grind` (#27654)

* feat: use grind in Nat/Int parity results (#27661)



Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>

* chore: update Mathlib dependencies 2025-07-31 (#27714)

This PR updates the Mathlib dependencies.

* feat(CategoryTheory/Adjunction): more results on adjoint triples. (#27650)

Lemmas about adjoint triples `F ⊣ G ⊣ H` where either `G` is fully faithful or `F` and `H` are.

* feat(Algebra/Ring/Idempotent): subtraction lemmas for idempotents and star projections (#25910)

This allows us to use subtraction with idempotents and star projections.

For idempotents `p,q`, `q - p` is idempotent when `p * q = p = q * p`.

For star projections `p,q`, `q - p` is a star projection when either `p * q = p` or `q * p = p`. In a star-ordered ring, when `p * q = p` or `q * p = p` we get `p ≤ q`.



Co-authored-by: themathqueen <23701951+themathqueen@users.noreply.github.com>

* feat(gcongr): also use more general lemmas, closing extra goals with rfl (#26907)

This PR fixes an annoyance in tagging `gcongr` lemmas: if your function has `n` arguments in which to use congruence, then you would need to provide `2^n-1` `gcongr` lemmas. Now, it suffices to only tag the most general `gcongr` lemma, and in more specific cases, the extra goals will be closed using `rfl`.

While working on this, more issues with `gcongr` came up, and these all needed to be dealt with in the same PR:
- When applying a `gcongr` lemma, this should be done in the `reducible` transparency. The transparency was already bumped form `default` to `instances` after a zulip discussion ([#mathlib4 > gcongr unfold DFunLike.coe](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/gcongr.20unfold.20DFunLike.2Ecoe/with/482186693)). But I found that the same issue appears at `instances` transparency instead of `reducible`. MWE:
```
import Mathlib

open MeasureTheory
variable {α : Type*} (a : Set α) {μ : OuterMeasure α} {μ' : OuterMeasure α}

@[gcongr] -- remove this tag to make the last example work
lemma mono_outerMeasure (h : μ ≤ μ') : μ a ≤ μ' a := h a

example (h : μ ≤ μ') : μ a ≤ μ' a := by gcongr

variable [MeasurableSpace α] {ν : Measure α} {ν' : Measure α}

@[gcongr]
lemma mono_measure (h : ν ≤ ν') : ν a ≤ ν' a := h a

example (h : ν ≤ ν') : ν a ≤ ν' a := by
  with_reducible apply mono_outerMeasure
  set_option trace.Meta.isDefEq true in
  with_reducible gcongr
```
This aligns with the `congr!` tactic
- Using `reducible` transparency is not compatible with the approach of matching `varyingArgs`, because when comparing instance arguments, we need to use at least `instances` transparency. So, instead of storing the lemmas by `varyingArgs`, we sort them by the number of varying arguments, and simply try applying all the lemmas (which should be cheap in `reducible` transparency). This aligns with `congr`/`congr!`(/`simp`) which also tries all of the lemmas for the given constant.
- As a result of sorting the lemmas in the same way as `congr` lemmas, more recently added lemmas are now tried before older ones. This causes an issue which has to be solved by implementing a priority argument for the `gcongr` tag (similar to how `instance` and `simp` work), e.g.`@[gcongr high]`. This aligns with the `@[congr]` tag.

* chore(Analysis/Analytic): golf `isClopen_setOf_analyticOrderAt_eq_top` using `grind` (#27722)

* chore(Analysis/Calculus): golf `IsOpen.exists_smooth_support_eq` using `grind` (#27723)

* chore(Analysis/Calculus): golf `lhopital_zero_right_on_Ioo` using `grind` (#27724)

* chore(Analysis/InnerProductSpace): golf `maximal_orthonormal_iff_orthogonalComplement_eq_bot` using `grind` (#27725)

* chore(Analysis/SpecialFunctions): golf `posPart_negPart_unique` using `grind` (#27726)

* chore(Combinatorics/SetFamily): golf `familyMeasure_compression_lt_familyMeasure` using `grind` (#27727)

* chore(Data/QPF): golf `mem_supp` using `grind` (#27730)

* feat(RatFunc/Degree): intDegree_inv (#27625)


Add `intDegree_inv`, a lemma over `RatFunc` that states that the degree of the inverse of `x` is minus the degree of `x`.

* chore: remove old 2024-04 deprecations (#27713)

This PR removes some 15 month old deprecations. I forget why they weren't removed in previous cycles, but they seem okay to remove now.

* feat(GroupTheory/ArchimedeanDensely): locally finite linearly ordered groups are mul archimedean (#27410)

for CFT workshop

* chore(autolabel): label algebraic topology PRs separately (#27700)

[Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/345428-mathlib-reviewers/topic/New.20label.20for.20algebraic.20topology.20PRs.3F/with/524724457) in the mathlib-reviewers stream

* chore: deprecate cc tactic (#27710)

This PR deprecates Mathlib's `cc` tactic. (This is a port of Leo's implementation in Lean 3.)

While `cc` does support some goals which `grind` doesn't (some by design for performance reasons, others we should catch up soon anyway), Mathlib hasn't ever relied on this additional functionality, and we don't know of downstream libraries using it. If we discover such users, I'd like to first have a change to migrate them to `grind`, and then we can decide whether to cancel the deprecation, or spin out `cc` into a standalone library.

* chore: incomplete removal of >6 month old deprecations (#27717)

We need a better process for this.

Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>

* docs(Topology/Perfect): Mention dense-in-itself (#25343)

The file `Mathlib/Topology/Perfect` defines a "nonstandard" predicate `Preperfect C` to mean that every point of `C` is an accumulation point of `C`. This property already has a name, it is called [dense-in-itself](https://en.wikipedia.org/wiki/Dense-in-itself). This PR adds this name to the docs.

* feat: lemmas on the volume on `I` applied to intervals  (#27513)

- `instance : NoAtoms (volume : Measure I)`

- `(volume : Measure I) s = volume (Subtype.val '' s)`

- `(volume : Measure I) (Icc x y) = ENNReal.ofReal (y - x)`

- `(volume : Measure I) (Ico x y) = ENNReal.ofReal (y - x)`

- `(volume : Measure I) (Ioc x y) = ENNReal.ofReal (y - x)`

- `(volume : Measure I) (Ioo x y) = ENNReal.ofReal (y - x)`

- `(volume : Measure I) (Iic x) = ENNReal.ofReal x`

- `(volume : Measure I) (Ici x) = ENNReal.ofReal (1 - x)`

- `(volume : Measure I) (Iio x) = ENNReal.ofReal x`

- `(volume : Measure I) (Ioi x) = ENNReal.ofReal (1 - x)`

- `(volume : Measure I) (uIcc x y) = edist y x`

- `(volume : Measure I) (uIoc x y) = edist y x`

- `(volume : Measure I) (uIoo x y) = edist y x`

Co-authored-by: Rémy Degenne <remy.degenne@inria.fr>



Co-authored-by: Gaëtan Serré <56162277+gaetanserre@users.noreply.github.com>

* chore(AlgebraicTopology/SimplexCategory): golf `factor_δ_spec` (#27615)

* chore: optimize code (#27669)

Following suggestions of @YaelDillies, optimize the code in `Analysis/Complex/Conformal.lean`. The optimizations were suggested during the review of #26839 but came in after Bors had already merged the PR.

* feat(Arctan): add more `simp` lemmas (#27719)

Also add some `positivity` extensions.

* feat(Topology/Order/Basic): lower set in well-order is open (#26928)

As well as the other analogous theorems.

* chore: split long file `DedekindDomain/Ideal.lean` (#27676)

This PR splits `Mathlib/RingTheory/DedekindDomain/Ideal.lean` into three parts:

* `FractionalIdeal/Inverse.lean` defines the `Inv` operator on fractional ideals, and proves basic results.
* `DedekindDomain/Ideal/Basic.lean` defines `IsDedekindDomainInv`, shows equivalence with `IsDedekindDomain` and provides unique factorization instances. This is sufficient for `ClassGroup.lean`.
* `DedekindDomain/Ideal/Lemmas.lean` defines `HeightOneSpectrum` and contains remaining lemmas.

Also upstream a lemma that doesn't refer to Dedekind domains.




Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

* feat: `f '' s = f ⁻¹' s` for an involution `f` (#27746)

* chore: scope or remove some instances (#27592)

Per @fpvandoorn's suggestions at [#mathlib4 > type-class inference slow/timing out @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/type-class.20inference.20slow.2Ftiming.20out/near/530602780).

Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

* chore: move and golf Subring.mem_closure_image_of (#27652)

* feat(to_additive): improve (error) message of `(reorder := ...)` (#27692)

This PR improves the ease of use of `(reorder := ...)` for the `to_dual` tactic.

It also supersedes #27452, by removing the unneeded `List.reverse`.

* feat: mapping the product measure by eval (#27721)

The evaluation function at `i` is `QuasiMeasurePreserving` from `Measure.pi μ` to `μ i`. If the `μ i`s are probability measures, then it is `MeasurePreserving`.

* chore(RingTheory/Spectrum/Prime/LTSeries): fix author name and golf (#27760)

Fix author name and golf.



Co-authored-by: Yongle Hu <140475041+mbkybky@users.noreply.github.com>

* doc: fix some typos in module docstrings (#27761)

Fix some typos in module docstrings.



Co-authored-by: Yongle Hu <140475041+mbkybky@users.noreply.github.com>

* feat: basic translations between `X →o Y` and `X ⥤ Y` (#26415)

Adds basic definitions translating between `X →o Y` and `X ⥤ Y` where `X` and `Y` are regarded as `Preorder` categories.

* feat: more RestrictedProduct API (#25715)

A constructor, more algebra boilerplate (e.g. `SMul ℕ` on a restricted product of `AddMonoid`s, restricted product of `CommMonoid`s is a `CommMonoid`, restricted product of `R`-modules wrt `R`-submodules is an `R`-module, variant of `map` when the index set doesn't change). 

From the FLT project.

* feat(Valued/LocallyCompact): do not require RankOne to show IsDVR (#27412)

for `isDiscreteValuationRing_of_compactSpace`
for the CFT workshop



Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>

* feat(RingTheory/ValuativeRel): IsRankLeOne when there is a compatible Zm0 or NNReal valuation (#27183)

and then provide it for Q_[p]

* chore: remove some duplicate instances (#25410)

I have a program that finds duplicate instances, as described at [#mathlib4 > duplicate declarations](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/duplicate.20declarations/with/518941841)

This PR is a start at fixing these in Mathlib.

* chore(Order/ConditionallyCompleteLattice/Basic): `@[gcongr]` (#27291)

This PR adds low priority `@[gcongr]` tags about conditional infima/suprema.

* feat: start using `grind` in `Set` API (#27670)

This PR starts adding `grind` annotations to theorems about `Set`, and simplifying proofs. Neither effort is exhaustive in any of the files I touch here; it's just a start.

* chore(NumberTheory/FLT): golf `not_minimal` (FLT/Four) using `grind` (#27558)

* chore(LinearAlgebra/RootSystem/GeckConstruction): golf `lie_e_f_ne` using `grind` (#27560)

* chore(SetTheory/ZFC): golf `mem_pairSep` using `grind` (#27564)

* chore(Tactic/Simproc): golf entire `exists_of_imp_eq` using `grind` (#27565)

* chore(Algebra/MvPolynomial): golf `vars_sum_of_disjoint` using `grind` (#27671)

* chore(Data/List): golf `mem_ofFn'` using `grind` (#27729)

* chore(Data/Set): golf `ncard_le_one_iff_eq` using `grind` (#27731)

* chore(Geometry/Euclidean): golf `oangle_sign_smul_add_right` using `grind` (#27733)

* chore(Geometry/Euclidean): golf `exists_forall_dist_eq_iff_exists_excenterExists_and_eq_excenter` using `grind` (#27734)

* chore(LinearAlgebra/LinearPMap): golf `mem_range_iff` using `grind` (#27764)

* chore(LinearAlgebra/Matrix): golf `det_eq_of_forall_row_eq_smul_add_const_aux` using `grind` (#27765)

* chore(LinearAlgebra/RootSystem): golf `chainBotCoeff_mul_chainTopCoeff` using `grind` (#27766)

* chore(MeasureTheory/Function): golf `MeasureTheory.aemeasurable_of_exist_almost_disjoint_supersets` using `grind` (#27767)

* chore(MeasureTheory/Function): golf `map_lintegral` using `grind` (#27768)

* chore(MeasureTheory/Integral): golf `map_setToSimpleFunc` using `grind` (#27769)

* chore(MeasureTheory/PiSystem): golf `mem_generatePiSystem_iUnion_elim` using `grind` (#27770)

* chore(NumberTheory/BernoulliPolynomials): golf `sum_bernoulli` using `grind` (#27771)

* chore(Order/ConditionallyCompleteLattice): golf `Set.Finite.ciSup_lt_iff` using `grind` (#27772)

* chore(Probability/Independence): golf `iIndepFun.indepFun_finset` using `grind` (#27773)

* chore(RingTheory/MvPolynomial): golf `disjoint_filter_pairs_lt_filter_pairs_eq` using `grind` (#27774)

* chore: fix typo in nightly_detect_failure.yml (#27793)

* chore(Topology/MetricSpace): golf `mem_uniformity_dist` using `grind` (#27784)

* chore(RingTheory/Polynomial): golf `dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_isEisensteinAt` using `grind` (#27775)

* chore(RingTheory/Polynomial): golf `prod_X_add_C_coeff` using `grind` (#27776)

* chore: update Mathlib dependencies 2025-08-01 (#27797)

This PR updates the Mathlib dependencies.

* feat(Topology): {Nat,Int).cast_continuous (#27662)

* chore: deprecate `Module.Free.repr` (#24891)

One should instead use `(Module.Free.chooseBasis R M).repr`.

* Review comments

---------

Co-authored-by: Scott Carnahan <128885296+ScottCarnahan@users.noreply.github.com>
Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
Co-authored-by: Christian Merten <christian@merten.dev>
Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com>
Co-authored-by: Anne Baanen <vierkantor@vierkantor.com>
Co-authored-by: Amelia Livingston <al3717@ic.ac.uk>
Co-authored-by: 101damnations <101damnations@github.com>
Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>
Co-authored-by: Paul Lezeau <paul.lezeau@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: fweth <klausgy@gmail.com>
Co-authored-by: Pierre Quinton <pierre.quinton@gmail.com>
Co-authored-by: Weiyi Wang <wwylele@gmail.com>
Co-authored-by: Aaron Liu <aaronliu2008@outlook.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>
Co-authored-by: Xavier Généreux <xaviergenereux@hotmail.com>
Co-authored-by: euprunin <euprunin@users.noreply.github.com>
Co-authored-by: Yakov Pechersky <ffxen158@gmail.com>
Co-authored-by: Bolton Bailey <boltonb2@illinois.edu>
Co-authored-by: Bolton Bailey <bolton.bailey@gmail.com>
Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk>
Co-authored-by: Cameron Zwarich <cameron@lean-fro.org>
Co-authored-by: Thomas Browning <tb65536@uw.edu…

…o separate file (leanprover-community#27337)

This PR moves material that uses `MonoidWithZero` into a separate file.