Changelog

chore(Analysis/InnerProductSpace/Dual): weaken assumptions to SeminormedAddCommGroup (#17416) …

feat(CategoryTheory/Limits): generalize universes for preserving finite products (#17408)

feat (Mathlib/SetTheory/Ordinal/Arithmetic): add bounded recursion on ordinals (#16663) …

feat: not_odd_zero for Nat and Int (#17419) …

chore: update Mathlib dependencies 2024-10-04 (#17414) …

feat(AlgebraicGeometry): add `resLE` (#17264) …

chore(RingTheory/Valuation): change implicitness in `Valuation.IsEquiv` lemmas (#17051) …

feat(AlgebraicGeometry/EllipticCurve/NormalForms): some normal forms of elliptic curves (#16864) …

chore(NumberTheory/LucasPrimality): golf theorem (#16848)

feat: Adding/removing an element from a product of finsets (#7898) …

chore: make `Integrable.of_finite` have no explicit argument (#17323) …

feat(Algebra/Group/Equiv): add two simp lemmas for `MulEquivClass` (#17085) …

chore(*): assume `Subsingleton Mˣ` instead of `Unique Mˣ` (#17391) …

chore(Analytic/CPolynomial): move&generalize some lemmas (#17390) …

chore(Galois/Basic): `Fintype` → `Finite` (#17382)

chore: generalise even more lemmas from `LinearOrderedField` to `GroupWithZero` (#17378)

ci(update_dependencies_zulip): Add actionable message when lake update fails (#17331)

chore: `Set.divisionCommMonoid` scoped earlier (#17301) …

feat: `a = cast e b ↔ HEq a b` (#17294) …

feat(Data/Multiset/Basic): add lemma on `Multiset` (#17273) …

feat(NumberTheory/RamificationInertia): ramification index and inertia degree in tower of algebras (#17160) …

chore(Data/Set): split Data/Set/Function (#17091) …

feat(Data/Int/WithZero): add WithZeroMultIntToNNReal (#15741) …

feat(CategoryTheory): lemmas about `descOfIsLeftKanExtension` for pointwise left Kan extensions (+dual) (#17383)

chore(CompHausLike): add constant morphisms (#17381)

feat (Analysis/Normed/Group): ultrametric normed groups are nonarchimedean (#17262) …

chore: Delete declarations deprecated in 2023 (#17193) …

feat(Condensed): discrete condensed modules are given by locally constant maps (#15569) …

feat: the canonical bilinear form of the root system of a Lie algebra is the Killing form (#17392) …

refactor(CategoryTheory): generalize universes for representable functors (#17389) …

chore(Profinite): add Fintype instances (#17380)

feat(RingTheory): target local closure of property of ring homomorphisms (#17032) …

feat(Data/Finset): right elements of a finset in the sum type (#17014)

feat(Topology/Group): Open normal subgroup (#16980) …

feat(Tactic/Algebraize): add algebraize tactic (#16217) …

chore: bump toolchain to v4.13.0-rc3 (#17401)

feat: the cosine of `π / 5` is `(1 + √5) / 4` (#17393)

chore: update Mathlib dependencies 2024-10-04 (#17397) …

ci(nightly_detect_failure): add actionable message in case of failure (#17329) …

feat: if a function is analytic on a set, its derivative also is, even if the space is not complete (#17221) …

refactor(Algebra/Field/Subfield): minor golfing (#17376)

feat(RingTheory): define two-sided Jacobson radical (#17341) …

feat: Order properties of `Pi.single` (#17281) …

feat: Big operators indexed by an interval (#17280) …

feat: Order instances for `MulOpposite`/`AddOpposite` (#17201) …

feat(Data/*/Sort): lemmas on sorted lists (#16078) …

chore(Finset): remove old-style spellings (#17327) …

chore: bump toolchain to v4.13.0-rc2 (#17377) …

chore: Rename `UniformEmbedding` to `IsUniformEmbedding` (#17295) …

refactor: Let `positivity` handle `ENNReal`-valued `ofNat` (#17212) …