Changelog

feat(Data/Nat/Factorization/Defs): more theorems about `f.prod (· ^ ·)` (#36792)

feat(Analysis/InnerProductSpace/Spectrum): eigenspaces of a compact selfadjoint operator exhaust the Hilbert space (#36520) …

feat(CStarAlgebra): lemmas related to `CFC.rpow` and `IsStrictlyPositive` (#36784) …

chore(Combinatorics/SimpleGraph): move `WalkDecomp` and `WalkCounting` to `Walks` (#36819) …

feat: torsion of an affine connection (#36285) …

feat(Combinatorics/SimpleGraph/LapMatrix): {`adjMatrix`/`degMatrix`/`lapMatrix`} are Hermitian (#36335) …

feat(ProbabilityTheory): Conditional Jensen's Inequality (#27953) …

feat: generalize Hölder's inequality for sums to `Real.HolderTriple` (#35198) …

feat: Poisson Integral Formula for harmonic functions (#36278) …

feat: introduce canonical factors, a.k.a. "Blaschke factors", as used in complex analysis (#36264) …

feat: monotonicity of D^n(U) in n and in U as CLMs (#32401)

chore: golf using `fin_omega`, `simp_all` and `grind +splitIndPred` (#36509) …

feat(Algebra): injective dimension equal supremum of localized module (#32033) …

feat: added simp lemmas to LieRinehartAlgebra (#36650) …

feat(Adjoin/Polynomial/Bivariate): IsAlgebraic.adjoin_singleton (#35874) …

fix: update link to mathlib4 naming conventions (#36812) …

chore(IsFractionRing): make argument explicit (#36655) …

feat: ContinuousLinearMap.continuous_of_continuous_uncurry (#36776) …

feat: add `IsUniformEmbedding.of_comp` (#36771) …

refactor(Analysis/Lp): EuclideanSpace.single -> PiLp.single (#36685) …

feat(Analysis/Lp): simp lemma for LinearMap.det and toLpLin (#36661) …

feat: binomial random variables (#28248) …

feat: differentiation of test function as a CLM (#31809)

refactor(Combinatorics/SimpleGraph): make the vertex argument explicit in `Walk.rotate` (#36800) …

feat(ModularForms): (normalized) derivative of modular forms (#36405) …

feat(Algebra/Order/Floor/Ring): generalize `Int.abs_sub_lt_one_of_floor_eq_floor` (#36805) …

chore(Algebra/SkewMonoidAlgebra/Basic): generalize lemmas from Monoid to Mul (#36737)

feat: `IsCofinal s` implies `IsCofinal (f '' s)` (#36715)

chore(Algebra/Group/InjSurj): clean up instances (#36413) …

chore(CategoryTheory): Remove `erw` and `respectTransparency` (#36801) …

feat(Algebra/MonoidAlgebra): explicit conversion functions to/from `Finsupp` (#36762) …

perf(RingTheory/Ideal/Quotient/HasFiniteQuotients): fix the `HasFiniteQuotients` instance (#36535) …

chore(Topology): rename lim -> Filter.lim and limUnder -> Filter.limUnder, and make a lemma protected (#36522) …

feat(MeasureTheory): add `continuousWithinAt_Ici/Iic_primitive_Ioi/Iio` and `continuousOn_Ici/Iic_primitive_Ioi/Iio/Ici/Iic` (#34966) …

feat: processes with independent increments (#36718) …

doc(AlgebraicTopology/DoldKan): fix typos (#36765) …

chore: replace `aesop` with `grind` where the latter is significantly faster (#35947) …

feat(NumberTheory/RatFunc/Ostrowski): prove Ostrowski's theorem for K(X) (#30505) …

feat(Data/Nat/Factorization/Divisors): calculate divisors using prime factorization (#34554)

chore: remove 712 more `set_option backward.isDefEq.respectTransparency` (#36791) …

feat(Tactic/FastInstance): skip mkAuxTheorem for proof fields when types agree at instances transparency (#36717) …

feat(Computability.Primrec.List): add primrec proofs for drop, takeWhile, and dropWhile (#36473) …

doc(SetTheory/Ordinal/Arithmetic): improve documentation (#35858) …

chore: mark `toSubfield`, `toSubmodule`, `toSubring` as `reducible` (#36395) …

feat: Nat/Int casts on char two rings (#34622)

feat(SetTheory/Ordinal/Basic): the `#s`-th element of `α` is an upper-bound for the set's mex (#36539) …

feat(SimpleGraph): taking twice from a walk equals taking the minimum (#35292) …

feat(Analysis/Normed): Schauder basis definition and characterization via projections (#34209) …

feat(CategoryTheory/ObjectProperty/Kernels): Object properties of (co)kernels (#36481) …

feat(Mathlib/Analysis/Asymptotics/Defs): congr lemmas for IsBigO* (#35745) …