Changelog

feat: lemma concerning for `‖cfc f a‖ < c` (#18361)

chore: remove a few unused variables (#18362) …

fix(LongestPole): windows paths compatibility (#18341) …

feat: `cfc_tsub` for `ℝ≥0` functions (#18360)

refactor(RingTheory/Ideal/Pointwise): Generalize to semirings (#18355) …

feat(CategoryTheory) : (Co)structured arrow as a functor to Cat (#18298) …

feat(RingTheory/IsLasker): strength primary decomposition to a minimal one (#18296) …

feat(RingTheory): generalize `Ideal.IsPrimary` to submodules (#17073) …

chore: update Mathlib dependencies 2024-10-28 (#18350) …

chore(Algebra/Group/Subgroup): split off `Defs` file (#18340) …

doc(Analysis/RCLike/Basic): correct link in documentation (#18343)

feat(Topology) define jacobson spaces (#18243)

feat(Algebra/FreeMonoid): set of symbols appearing in an element of the free monoid (#18036) …

feat(Archive/Imo): formalize IMO 1982q1 (#16883) …

feat(NumberField/CanonicalEmbedding): define the `negAt` map (#18234) …

feat: matrices with fixed determinant (#16159) …

feat(RingTheory/Flat): faithfully flat ring maps (#15014) …

chore: remove almost all `import Lean` (#18276) …

chore: remove unused vars (#18337) …

chore(CategoryTheory/Functor): dualize `OfSequence` (#18325)

feat(AlgebraicGeometry/PrimeSpectrum): prime spectrum of jacobson rings (#18242)

feat: `a / b < 0 → 0 ≤ a → b < 0` (#18260)

feat: `EReal.forall`, `EReal.exists` (#18301)

doc: fix typo in perfect numbers module docstring (#18334)

feat(Algebra/Module): presentation of modules (#18295) …

chore: remove some `maxHeartbeats` bumps that are no longer needed (#18324) …

feat: indicator of a clopen set as a bounded continuous function (#18291) …

chore: remove more variables (#18323) …

chore: cleanup skipAssignedInstances flags (#18320)

feat: add by how many modules imports grew (#18303) …

feat(Algebra/Order/Field/Basic): add Nat cast lemmas (#18171) …

chore: remove some no-longer-needed backwards compatibility flags (#18319)

feat: lake exe unused (#18156) …

chore: some `erw`s that can become `rw` for free (#18322) …

chore: move contents of Data.Finite.Basic earlier (#18316)

chore: import Mathlib.Init in all files (#18277) …

feat(RingTheory/Ideal/Maps): lemmas of ring isomorphisms act on ideals (#18249) …

feat(RingTheory/LinearDisjoint): definition and properties of linearly disjoint of subalgebras (1) (#17820) …

chore: Rename `Embedding` to `IsEmbedding` (#18133) …

chore(Data/List): move the definition of finRange to Defs (#18312)

feat: `ext` lemmas for `MultilinearMap` (#18308) …

chore: remove unused variables (#18305) …

chore(Wiedijk100Theorems): clean up SolutionToCubic (#18299) …

feat: `ZMod`-module lemmas (#17693) …

chore: split Data.Set.Basic (#18317) …

chore: split Mathlib.Topology.Algebra.UniformGroup (#18311) …

feat: gluing measurable functions along measurable embeddings (#18287)

refactor: generalize AddSubmonoid Mul lemmas to SMul (#18278)

feat(Algebra/Polynomial/AlgebraMap): add `algEquiv(OfCompEqX|AevalXAddC)_(eq_iff|symm)` (#18257)

feat(FieldTheory): define induced action of subfields and intermediate fields (#18141) …