Changelog

feat(Logic/Function): define `Function.IsConstOn` predicate (#45867) …

chore(Order): tweak naming and simp NF of some `OrderIso`s (#45714) …

chore(Dynamics/Flow): generalize typeclass assumptions (#45804)

refactor(Geometry/Euclidean): promote Heron's formula to main mathlib (#44148) …

feat(PowerSeries/Derivative): add some lemmas (#43305) …

chore(Topology/Connected/TotallyDisconnected): use a typeclass param in `PreconnectedSpace.constant` and respell using `IsConst` (#45848) …

chore(RingTheory): remove unused hypothesis (#45696) …

chore(Util/Export): deprecate (#45357) …

feat({Topology,MeasureTheory}): instances for `Additive`/`Multiplicative` (#45174) …

feat(Combinatorics/SimpleGraph/Maps): more `map`/`comap` API (#42370)

feat(Analysis/Complex): `(a * b) ^ r = a ^ r * b ^ r` (#45726) …

feat(Combinatorics/SimpleGraph/Paths): length of closed a walk/trail isn't `1`/`2` (#41633) …

feat(SimpleGraph/Hamiltonian): a graph is Hamiltonian iff there's a Hamiltonian path with adjacent endpoints (#41393)

chore(Order): remove unused hypothesis (#45693) …

chore(LinearAlgebra/Matrix): add api for compatibility between `reindex` and `map` for `GL` and `Matrix` (#45519)

chore(LinearAlgebra): remove unused hypothesis (#45690) …

feat(LinearAlgebra/Matrix/Reindex): add `Matrix.reindexStarAlgEquiv` (#45199) …

feat: use `IsApply` for `AffineMap` and `AffineIsometry` (#45599) …

feat(MeasureTheory): add `IsAtom` and `NoAtoms` (#45666) …

chore: correct naming of coercion lemmas about coeIdeal (#45832) …

feat: `isInvertible_fderivWithin_writtenInExtChartAt` (#44843) …

feat: `@[gcongr]` for `eq_top_mono` and friends (#44334) …

feat: use `IsApply` for `Poly` (#45535)

feat: add `List.insertIdx_eraseIdx_getElem_perm` (#41308) …

feat(LinearAlgebra/Matrix): add the `prodEquiv` for `Matrix`, `GL` and `SL` (#44876)

chore(Topology/Instances/EReal/Lemmas): golf using positivity and gcongr (#45859) …

feat(Data/{D,}Finsupp/WellFounded): weaken `AddMonoid` to `Zero` in `WellFoundedLT` instances (#45793)

chore: golf using finiteness (#45749)

chore: remove trailing newlines in doc-strings (#45741) …

feat(Data/Set/Card): `ncard` of `image2`, and sets of a given `ncard` (#45617) …

feat: use `IsApply` for `OneHom` (#45472)

feat(Geometry/Convex): segments in convex space (#44799) …

feat(Logic/Relation,Order/WellFounded): lemmas about `Acc`, `WellFounded`, and `Relation.Map` (#44696) …

chore(Combinatorics/SimpleGraph/Girth): golf `egirth_top` using `cycleGraph` (#41336) …

feat(Combinatorics/SimpleGraph/Paths): some lemmas about inducing walks (#40967) …

feat: the definition of a KSheaf on a T2 Space (#40953) …

feat: interaction between `WithBot.succ` and `Order.pred` (#45582)

chore: golf some `conv` proofs (#45393) …

feat(Lean/Quote): restore `Quote` instances for `Int` and `Rat` (#44786) …

refactor: make `InfinitePlace.Completion` an `abbrev` (#45508) …

chore(Analysis/Calculus/VectorField): fix order of `V` and `W` in `fderiv_apply_lieBracket` lemmas (#45860) …

chore(Algebra/Order/Monoid/WithTop): generalize typeclass assumptions (#45803)

fix(Data/ENat/Defs): derive `Repr` for `ℕ∞` (#45761) …

feat: `Dyadic` is an ordered ring (#43038) …

chore(Algebra/Order/Group/Indicator): generalize typeclasses (#45805)

feat: simultaneous Dirichlet approximation theorem (#45646) …

feat(Analysis/Complex): arg(x*y) and log(x*y) for more cases (#45644) …

feat(Topology/Instances/AddCircle): `Infinite (AddCircle p)` for a densely ordered group (#45575)

chore(Algebra/Polynomial): parse `R[X]` as `R` + `[` + `X` + `]` (#45573) …

chore(Algebra/GroupWithZero/Units/Basic): rename three lemmas `'` -> `₀` (#43858) …