Changelog

feat: generalize `TwoSidedIdeal.matricesOver` to `RingCon` (#23641) …

feat: `PiFin.mkLiteralQ` and `Matrix.mkLiteralQ` (#24101) …

feat(BigOperators/Ring): add `Finset.prod_neg` (#24146)

feat(Combinatorics/SimpleGraph): miscellaneous walk lemmas (#22242) …

feat: Nat.toDigits_length (#24126) …

fix(ByContra hover): hover over by_contra! gets its doc-string back (#24087) …

chore: replace mono by gcongr (#23968) …

feat: add lemma `Submodule.length_lt` (#24133) …

feat(Interval/Finset/Fin): add lemmas about `Finset.image` (#23420) …

feat: `x.swap < (b, a) ↔ x < (a, b)` (#24124)

chore: deprecate the file `AnalyticManifold` (#20979) …

feat: add a `ToExpr` instance for `Multiset` (#24014) …

chore: automatically additivize IsScalarTower (#24115)

feat: additivise `Irreducible` (#22904) …

chore(Topology.Algebra.Valued.WithVal): clean up typeclass assumptions (#24125) …

chore: cleanup API around order of univariate power series (#24072) …

feat (RingTheory/PowerSeries/Order) : compute order of power and generalize (#23993) …

chore: remove TODO from docstring (#24111) …

fix: homeomorphisms->homomorphisms (#24097)

fix(nolints.yml): continue gracefully if no changes were found (#24110) …

feat(Lean/ToExpr): add helper functions to create `Expr` for finsets/sets/multisets (#23025) …

feat(NumberField/CanonicalEmbedding/NormLeOne): compute the volume of `NormLeOne` (#22777) …

feat(NumberField/Discriminant): better lower bound for totally complex number fields (#24076)

chore(RingTheory): fix variable in FilteredAlgebra.Basic (#24071) …

chore(Fin): fix some `@[simp]` lemmas (#23967) …

feat: definition + basic results for chains / strings in root pairings (#24077)

fix(nolints.yml): move `print Lean version` step after the installation of Lean (#24088) …

feat(CategoryTheory/Limits): preservation of multicoequalizers (#22205)

feat(CategoryTheory/Limits): multicoequalizers attached to linear orders (#22203) …

chore(Archimedean/Basic): minor cleanup (#23854)

chore(CategoryTheory/Over): fix name of `Under.pullbackComp` (#24084)

doc: correct scope name (#24085)

chore: exchange `Nat.sub_lt_iff_lt_add` and `Nat.sub_lt_iff_lt_add'` (#24080) …

feat(CategoryTheory): `ChosenFiniteProducts (Over X)` (#21399) …

chore(BumpFunction/Convolution): drop an assumption (#24063) …

feat(LpSeminorm/Basic): generalise monotonicity section to enorm (#23707) …

feat (Yoneda): (co)representing objects are unique up to iso (#24059) …

chore(Finsupp/Interval): remove `open scoped Classical` (#24055) …

feat: add characterisation of closed interval for locally-finite conditionally complete linear orders (#23910)

chore: split `MeasureTheory.Integral.SetToL1` (#24075) …

feat: a binary fan in `Over X` is the same thing as a pullback cone to `X` (#23723) …

feat(RingTheory/LocalRing): results for non-local rings (#24043)

chore: split `MeasureTheory.Integral.SetIntegral` (#24070) …

chore: move and rename `eval_of_algHom` (#23952) …

chore(Analysis/Convex/Combination): remove `open scoped Classical` from theorems (#24057) …

chore(*): rename more type vars for *rings (#24022)

feat(Set): restricting the identity function (#23995)

feat(Topology): closure of subsingleton is self (#24062) …

chore: golf copy of Pi.single (#24061)

feat(Algebra/Algebra/Subalgebra): `Algebra.adjoin_singleton_le` (#24048) …