Changelog

chore: update Mathlib dependencies 2026-10-01 (#44386) …

ci(cache): bound the snapshot run lookup by creation date (#44171) …

fix(CategoryTheory/Monoidal/Internal/Types): remove superfluous instance (#44399) …

chore(Calculus/FDeriv/Add): reorganize the file (#44203) …

chore(Combinatorics/Derangements/Finite): remove superfluous instance (#44395) …

chore(Topology/DiscreteQuotient): remove duplicate instance (#44385) …

chore(Algebra/Lie/Subalgebra): fix instance diamond in LT instance (#44382) …

chore: fix an implicit reducible diamond in shrinked normed spaces (#44130) …

feat(Data/Sym/Sym2/Card): cardinality theorems about `Sym2 α` (#36442)

refactor(CategoryTheory): use quadrifunctors for the localized pentagon (#43009) …

chore(Order/Partition/Finpartition): deprecate `ofPairwiseDisjoint` (#40274) …

perf: disable the unreachable tactic linter (again) (#44391) …

feat(SetTheory/Ordinal): definition of addition and multiplication (#43588) …

chore(GroupTheory/Perm/*): switch from `ConjAct` to `MulAut.conj` (#44059) …

fix(Order/Heyting/Regular): fix `Lattice` instance diamond (#41776) …

chore(CategoryTheory): remove duplicate instance on `CostructuredArrow` (#44197) …

perf(Linter/UnusedTactic): replace `IO` with `BaseIO` (#44377) …

chore: remove `linear_combination'` tactic (#28925) …

chore(MeasureTheory/Integral/DominatedConvergence): automated extraction from #26479 (#44380) …

feat(LinearAlgebra/Matrix/Rank): linearly independent rows give a surjective mulVec (#43956) …

ci(weekly-lints): pass the build status to the Zulip report (#43551) …

feat: add `{IsUnit}.map_ringInverse` (#44087) …

feat(Algebra/Divisibility/Basic): divisibility in opposite semigroups (#44366) …

refactor(SetTheory/ZFC): make `Class` an `abbrev` for `Set ZFSet` (#43467) …

feat(Topology/Algebra): continuity of composing by a `ContinuousAffineMap` (#43339) …

feat(LinearAlgebra/Dimension/Constructions): `Set.ncard` version of four lemmas (#44359) …

chore(Algebra/Group/Torsion): deprecate `zpow_eq_zpow_iff'` (#44349) …

chore: rename `LinearMap.baseChange_eq_ltensor` to `baseChange_eq_lTensor` (#44327) …

feat(LinearAlgebra/LinearIndependent/Basic): promote `LinearIndepOn.id_imageₛ` to iff, and add `smul_set` version (#43487) …

chore: fix implicit reducible diamond in faces lattice (#44127) …

fix(GroupTheory/Subgroup/Center): make the additive version of commGroupOfCenterEqTop instance_reducible (#44120) …

feat(Algebra/Star/Basic): class for `star x * x = 0 → x = 0` (#44080) …

chore(LinearAlgebra/Matrix/NonsingularInverse): generalize some lemmas from `Field` to `IsArtinianRing` (#44054) …

feat: in characteristic 0, precomposition by a linear map is analytic on the space of alternating maps (#43338) …

chore: complete generalization of oneLePart lemmas to DivInvMonoid (#41584) …

feat(Combinatorics/SimpleGraph/Hamiltonian): a graph with a Hamiltonian path is connected (#41435) …

feat(Geometry/Euclidean): unoriented angle eq of oriented angle eq (#40498) …

refactor(Algebra/Group): fix the definition of torsion-free non-abelian groups (#42407) …

ci: remove steps that consider state from earlier jobs (#44357) …

chore(Algebra): golf proof `Polynomial.aeval_algHom_apply` (#44337)

feat(LinearAlgebra/Matrix): add Sylvester's rank inequality (#43065)

chore(Topology/Homotopy/Lifting): fix typos `Iff` (#44330) …

feat(Algebra/Lie/Ideal): add coercion and norm_cast attributes for Lie Ideals (#44295)

feat(CategoryTheory): express monoidal pentagons using quadrifunctors (#43008) …

feat(Algebra/Homology/ShortComplex): pullbacks and pushouts of short exact sequences (#44229) …

feat: restricted multivariate power series as its own type and some missing API lemmas (#42867) …

chore(*): turn `convert!` into `convert` where appropriate (#44324) …

feat(Analysis/Subadditive): multiplicative Fekete's lemma (#42605) …

chore(Basic): move `FunLike` from Data (#43253) …

chore: extract lemma from `Cardinal.mul_self` (#44006) …