Changelog

feat: an equality condition for AM-GM inequality (#19435) …

chore: update Mathlib dependencies 2024-12-02 (#19672) …

chore: bump toolchain to v4.14.0 (#19673)

feat: `Polynomial.map f` strictly decreases the degree if `f p.leadingCoeff = 0` (#19411) …

ci(dependabot.yml): use glob syntax in config... (#19662) …

fix(FieldTheory/AlgebraicClosure): `algebraicClosure.AlgEquiv.algebraicClosure` -> `AlgEquiv.algebraicClosure` (#19642)

chore: move `Topology.Support` to `Topology.Algebra.Support` (#19651) …

chore: add location of build.in.yml to directories checked by dependabot (#18712) …

chore: update benchmark runner for leanprover/lean4#5684 (#19656) …

chore(Algebra/Data/Order/Floor): remove todo on `fract_div_intCast_eq… (#19652) …

chore: remove PartENat from PowerSeries (#19622)

chore: delete deprecated lemmas (#19627) …

feat(NumberTheory): Abel summation (#19289) …

feat(Algebra/MvPolynomial/Degrees): degreeOf_mul_X_eq_degreeOf_add_one_iff (#17553)

feat(FieldTheory/Galois): Lemmas of galois theory (#16979) …

chore: update benchmark runner for leanprover/lean4#5684 (#19649) …

refactor(Algebra/Bilinear): generalize to non-commutative base rings (#19232) …

chore(scripts): update nolints.json (#19647) …

feat: introduce ENat.card, and use it in place of PartENat.card (#19624)

chore: don't import conformal maps in Behrend's construction (#19638)

feat(CategoryTheory): Relation between the Grothendieck construction and `AsSmall` (#19539)

chore: remove `normalizeScaleRoots` (#6183) …

chore: move definition of ENat and PNat out of Order.TypeTags (#19485) …

chore(RingTheory): split up `Algebraic.lean` (#19370) …

feat(CategoryTheory/SmallObject/Iteration): existence of objects (bot and succ cases) (#19047)

chore: fix names `{un}op_non{neg,pos}` (#19575)

feat(Algebra/Homology/Embedding): dualise extend (#19560) …

feat(Algebra/Homology): more duality results (#19559) …

feat(Algebra/Homology/Embedding): the canonical truncation functor `trunGEFunctor` (#19543) …

feat(Algebra/Polynomial/Roots): for a monic polynomial `p`, `p.roots.map f = (p.map f).roots` if `p.roots.card = p.natDegree` (#19430) …

chore: change associativity of `+ᵥ` from `infixl` to `infixr` (#19321) …

feat(LinearAlgebra/Matrix/Permanent): smul (#19307) …

feat(Algebra/Homology/Embedding): the left homology of an extension of homological complexes (#18502) …

chore: split out map_dvd (#19565)

refactor(AlgebraicGeometry/EllipticCurve/*): add `WeierstrassCurve.IsElliptic` and remove `EllipticCurve` (#18531) …

feat: update the `ContDiff` definition to integrate analytic functions in the hierarchy (#17152) …

chore(Filter/Prod): drop `Filter.prod`, use `SProd` instead (#18315) …

chore: update Mathlib dependencies 2024-11-29 (#19608) …

chore: update Mathlib dependencies 2024-11-29 (#19605) …

feat(AlgebraicGeometry): the small site associated to a morphism property (#18945) …

feat(NumberTheory/EllipticDivisibilitySequence): extend even-odd recursion to integers (#13786) …

feat: Label zulip PR links with awaiting-author emoji (#19599) …

feat(Combinatorics/SimpleGraph/Matching): add `IsCycles` and `IsAlternating` with basic results (#19250) …

chore: update Mathlib dependencies 2024-11-29 (#19598) …

fix: add `realm_emoji` (and `emoji_code`) to auto-zulip reactions (#19597) …

chore: update Mathlib dependencies 2024-11-29 (#19595) …

feat(Order/InitialSeg): initial segments preserve successor limits (#19053) …

refactor(Order/WellFounded): deprecate `WellFounded.succ` (#18238) …

chore(SetTheory/Ordinal/Basic): deprecate results on `WellOrder` (#18208) …

chore: bump toolchain to v4.14.0-rc3 (#19594) …