Changelog

docs(Konigsberg): fix grammar (#23208)

chore(*): see if timing out `simpNF`s have been fixed (#23202) …

feat: delaborator for finset builder notation (#22076)

feat(List): a list contains a single element iff it's a singleton (#20488) …

feat(Topology/Algebra/InfiniteSum/Order): positivity extension for infinite sums (#21557) …

feat: lemmas about `Measure.dirac` (#23071)

chore: deprime `induction'` in root files (#22533) …

chore: adjust hypothesis of mul_factorial_pred (#23160) …

chore: generalise `ENat.iInf_eq_zero` (#23180) …

chore: update Mathlib dependencies 2025-03-21 (#23174) …

feat(CategoryTheory/Enriched/Limits): add HasConicalTerminal (#23141)

feat(Data/Finset/Card): add `exists_mem_not_mem_of_card_lt_card` (#23172) …

chore(CStarAlgebra): fix outdated docstring (#23166)

chore: use known bounds to avoid runtime array checks (#23130) …

chore: review of `erw` in `Archive/` and `Counterexamples/` (#23168)

chore(Tuple/Sort): dualize `unique_monotone` to `unique_antitone` (#23046) …

feat(Algebra/Order/Floor): add nonnegativity / `Nat` casting lemmas for `Int.ceil` with weaker hypotheses (#22949) …

feat(Analysis/Asymptotics) `IsBigO.add_iff_left` and variants (#23059) …

feat: the Motzkin polynomial is nonnegative (#23170) …

chore(Topology/Order): use @[to_additive] (#22463)

feat(Set): lemmas about set difference (#22253) …

chore: remove >6 month old deprecations in `SetTheory` (#23164) …

chore: more continuity -> fun_prop replacements (#23151)

chore(Algebra/Group): split off big operators from `Pointwise/Finset/Basic.lean` (#23156) …

feat(AlgebraicTopology): endow `SSet` with notions of cofibrations and fibrations (#21118) …

chore(Order/Interval/Set): remove unneeded imports (#23158) …

chore(ENNReal): fix names (#23135) …

feat: `ENNReal.toNNReal` of `a - b` (#23134) …

feat: off-diagonal entries of Cartan matrices belong to `{-3, -2, -1, 0}` (#23077) …

feat: a reduced irreducible finite crystallographic root system has roots of at most two different lengths (#23007) …

chore: make the `A` arguments explicit in `{NonUnital}ContinuousFunctionalCalculus` (#23155) …

chore(Algebra/Group): split `iUnion`/`iInter` from long file `Pointwise/Set/Basic.lean` (#23152) …

chore(Data/Set): split long file `Function.lean` (#23149) …

feat: generalize Mathlib.LinearAlgebra.Matrix (#23144) …

feat(Combinatorics/SimpleGraph): define odd components (#22125) …

feat(Combinatorics/SimpleGraph): add DecidableRel instance for induced subgraph adjacency (#22080) …

feat: generalize *Finsupp* files (#23140) …

chore(Algebra/Group/Pointwise/Finset): drop unnecessary import (#23148) …

doc: provide an actual docstring to `MetricSpace` (#23123) …

chore(Topology): continuity -> fun_prop (#23136)

feat: corestrict an equivalence to a finset (#22534) …

feat: weaken differentiability assumptions of manifolds (#22804) …

chore: split `SetTheory.Game.PGame` (#23133) …

feat(Data/Finset/Sum): supremum over a disjoint union (#22983) …

chore: review of `erw` in `MeasureTheory/` (#23127)

feat(UniformSpace/Defs): mem_uniformity_ofCore_iff (#23115)

feat(Topology/UniformSpace): Is{Symmetric,Transitive}Rel.sInter (#23114)

feat(RingTheory): add `Polynomial.toMvPolynomial` (#22922)

chore: deprecate `Equiv.Set.ofEq` (#23119) …

chore(Logic/Equiv): split some chunks off large file `Equiv/Basic.lean` (#23099) …