Changelog

refactor: make TProd reducible (#12686) …

chore: deprecate redundant lemma List.find?_mem (#12677) …

chore: shorten proof of List.sizeOf_dropSlice_lt (#12678) …

doc(Tactic.Measurability): fixed copy paste error from continuity tactic docs (#12683) …

chore(Data/Set/Subset): simplify `image_val_sUnion` (#12654)

feat: Monotonicity of `Nat.cast : Nat → Fin (n + 1)` (#12652)

feat(Nat/Digits): ofDigits_add_ofDigits_eq_ofDigits_zipWith_of_length_eq (#12642)

Add constantCoeff_smul to RingTheory.PowerSeries.Basic (#12616) …

chore(Data/List): remove some long-deprecated theorems (#12350) …

feat: more NNRat lemmas (#12586) …

chore: reduce imports in ZMod.Basic (#12478) …

refactor(Data/PNat): better `OfNat` instance (#12420) …

feat(Analysis/PSeries): simp for summable_nat_pow_inv (#12423)

feat: add `HasSum f a → HasProd (exp ∘ f) (exp a)` (#12635) …

chore(LinearAlgebra/BilinearForm): Add missing deprecated dates (#12547) …

chore: remove temporary reviewdog fix (#12284) …

chore: replace `Quotient.exists_rep` with `induction` (#12471) …

fix: move convolution to MeasureTheory namespace (#12376) …

feat: clean-up `Topology.Order.IntermediateValue` (#12403) …

chore(Data/List/Perm): some nthLe -> get migration (#12397)

feat: Product of injective functions on sets (#12656)

chore: deprecate redundant lemma List.get?_injective (#12630) …

feat: lemmas about `Sigma.curry` (#12474) …

style(test/polyrith): adapt to mathlib4 style (#12091) …

docs: fix typo (#12659) …

feat: `a / b ≤ c ↔ a / c ≤ b` (#12622)

docs(RingTheory/Flat/Basic): remove completed TODO (#12612) …

feat: add `NonUnital{Star}AlgHom.restrictScalars` (#12657)

feat: Components of `Multiset.prod` over `α × β` (#12655)

feat: Locally linear graphs (#12526) …

feat: integration by parts for line derivatives and Frechet derivatives (#11937)

feat(Topology/Order/LawsonTopology): Introduce the Lawson Topology to Mathlib (#11710) …

refactor: new definition of `eigenvectorUnitary` (#11363) …

chore(LinearAlgebra): format/add dates to remaining deprecations (#12407) …

replay: #3604 for MonoidAlgebra (#12646) …

style: capitalizes file names in `Counterexamples` (#12615)

chore(Analysis/SpecialFunctions): `Real.rpow` -> `_ ^ _` (#12613)

chore: rename `cfc_map_quasispectrum` (#12640)

chore: cache warns about bad v4.8.0-rc1 toolchain (#12623)

refactor: simplify bundledAbstractFilteredClosure definition (#12603) …

chore: remove two `by exact` leftover from porting (#12626) …

perf(NumberTheory.NumberField.Basic): make `RingOfIntegers` a Type. (#12386) …

move: Rearrange basic algebraic subobject (#11104) …

feat(Topology/Algebra/InfiniteSum/Real): Add partition lemma (#12446) …

feat(MeasureTheory): add CountablySeparated (#12433) …

chore: make every Chebyshev polynomial argument a Gröbner basis computation (#12001) …

chore(Topology/Category): remove `ProfiniteMax` and `CompHausMax` (#12599) …

feat: enable dot notation for `HasEigenvalue` and the spectrum (#12580)

feat(Order/Interval/Finset/Box): add lemma (#12444) …

feat: Triangle removal (#12523) …