Changelog

chore: update Mathlib dependencies 2025-11-21 (#31918) …

feat: InfoTree API: `InfoTree.findSome`(`M`)`?` and `InfoTree.onHighestNode?` (#31725) …

feat: `privateModule` linter (#31820) …

feat(CategoryTheory): HasCardinalLT for MorphismProperty and ObjectProperty (#31421) …

doc: add missing spacing around doc code blocks (#31905) …

feat: ContinuousLinearEquiv.submoduleMap and friends (#31899) …

perf: de-instance some WithLp norm structures used for type synonyms (#31819) …

chore(Algebra/Group/Defs): missing `to_additive` (#31890)

chore(RingTheory): generalize to `Nonempty NormalizedGCDMonoid` in GaussLemma (#31874) …

feat(CategoryTheory): effective epi implies strong epi (#31860) …

chore(Analysis/{NormedSpace,Normed/Module}): migrate all remaining files (#30281) …

feat: basic lemmas about convexity over NNReal (#31887)

feat(Algebra/Lie/Extension): 2-cocycle from a Lie algebra extension with abelian kernel and a linear splitting (#31462) …

feat(Data): IsScalarTower for ZMod (#30833)

refactor(Algebra/Polynomial/Factors): rename `Factors` to `Splits` (#31878) …

feat(Algebra/Polynomial): misc lemma about mod (#31634) …

feat(Topology/UniformSpace/Closeds): uniform continuity of the singleton map (#31868)

refactor(Geometry/Euclidean/Sphere/Tangent): split out `orthRadius` (#31850) …

chore(Topology/Sets): use prefix naming for `toCompacts` in `simps` (#31591)

feat(CategoryTheory/ComposableArrows): compositions of 1 or 2 morphisms (#31588)

refactor(SetTheory/ZFC): deduplicate coercion to sets (#31287) …

feat: base change properties, direct sums, bases, modules of linear maps (#31240) …

chore: bump toolchain to v4.26.0-rc2 (#31877)

feat: inf of principal ideals is principal ideal of lcm (#31867) …

feat: `extract_goal` preserves explicit foralls (#31342) …

chore(Order/Basic): use `@[to_dual]` for `Preorder`/`PartialOrder` (#31852) …

chore: make `CLM.extend` total and define `LM.leftInverse` (#31799) …

feat: add CompleteAtomicBooleanAlgebra is order isomorphic to set of its atoms (#31724) …

feat: `@[gcongr]` for `indicator_le_indicator_of_subset` (#31847) …

doc(Tactic/MinImports): tidy backticks (#31861) …

feat: aestronglyMeasurable limit if converge in measure (#31791) …

feat: ofLp and toLp of a sum (#31353) …

feat(Topology/UniformSpace): define the Hausdorff uniformity (#31031) …

chore: remove use of `erw` in `Geometry.RingedSpace.OpenImmersion` (#31856)

feat(Algebra/Polynomial/Splits): remove the `RingHom` argument of `Splits` (#31631)

chore: remove use of `erw` in `Algebra.Homology.HomotopyCofiber` (#31855)

fix(rw??): `whnf` on equality hypotheses (#31609) …

chore(Order/Filter/CardinalInter): fix typos and polish docs (#31624) …

chore(Order/Defs/PartialOrder): fix typo in `decidableEqofDecidableLE'` (#31857) …

feat(GroupTheory/Perm/ClosureSwap): add slight generalization (#31570) …

feat: add `getD_comp_some` lemma for `Option` type (#31828) …

feat: add `splitOnP_append_cons` (#31825) …

feat(LinearAlgebra/AffineSpace/AffineSubspace/Basic): parallel lines in triples of points (#31712) …

feat(RingTheory/Etale): standard etale maps (#30867)

chore(GroupTheory/Subgroup/Centralizer): replace `centralizer (zpowers s)` with `centralizer {s}` (#30768) …

feat(Valuation): uniformizer of discrete valuation (#30259)

feat(Counterexamples): Peano curve (#26185) …

fix: explicitly enable header linter (#31849) …

chore(Order/Defs/PartialOrder): fix naming of `DecidableLE'` (#31816) …

feat(RingTheory/Valuation): monotonicity of mul wrt `SRel` (#31783)