Changelog

feat(Geometry.Euclidean.Sphere): inner product of chord with radius vector is negative (#36241) …

feat(Data/Finsupp/Order): `{map,emb}Domain` preserve tsub (#36369) …

chore: deprecate Turing files (#35609) …

feat(Mathlib/Analysis/Polynomial/MahlerMeasure): Mahler Measure estimate in terms of supNorm (#35280) …

feat(RingTheory/MvPowerSeries): introduce `rename` (#33188) …

chore: `Seminorm.continuous_from_bounded` -> `WithSeminorms.continuous_of_isBounded` (#36397)

feat(Analysis/CStarAlgebra/CFC/Order): conjugating with a star projection in a C*-algebra (#35997) …

feat(Analysis/Convex/SimplicialComplex): add AbstractSimplicialComplex + constructions (#33364) …

fix(Mathlib/CategoryTheory/Limits): fix naming of a lemma (#36455) …

feat(ENat): relate iInf of ENats to addition (#36452) …

feat(Analysis/Fourier): the Fourier transform as bounded continuous function (#35954) …

feat(Analysis/SchwartzMap): estimates for `Lp` and `BCF` norms (#35953)

chore(Tactic): rewrite `finiteness` tactic docstring (#35818) …

feat(Analysis/Distribution): Fourier multiplier (#34099) …

feat(Chebyshev/RootsExtrema): bound iterated derivatives of Chebyshev T on [-1, 1] (#34364)

feat(Analysis/SchwartzMap): translation of arguments (#35781) …

chore(GroupTheory/SpecificGroups/Alternating): clean up some proofs (#36450) …

chore(Analysis/InnerProductSpace): remove a hypothesis from LinearMap.IsSymmetric.card_filter_eigenvalues_eq (#36106) …

feat(Analysis/CStarAlgebra): `IsIdempotentElem a ↔ spectrum R a ⊆ {0, 1}` (#35916) …

feat(ENat): relate addition with strict inequality (#36454) …

feat(AlgebraicGeometry): intersection of affine opens in separated schemes is affine (#36453)

feat(Analysis): Eliminate a hypothesis on IsTheta.rpow (#36084) …

feat(Analysis/Distribution/ContDiffMapSupportedIn): Add a wrapper for fderiv on D_K^n (#30240) …

feat(Data/Multiset/Powerset): show injectivity and monotonicity of powerset (#35465) …

feat(Analysis/Convex): `extremePoints ℝ (closedBall x r) ⊆ sphere x r` (#35899) …

chore(Geometry/Manifold/MFDeriv/NormedSpace): use custom elaborators … (#36449) …

feat(Analysis/Normed/Operator): prove the Fredholm alternative (#35048) …

chore(Computability/Partrec): remove `linter.flexible` exceptions (#35682) …

fix(docs): deduplicate yaml key (#36001) …

fix: weird imports in `TestFunction.lean` (#36303)

feat: mfderiv_smul (#34263) …

ci: remove outdated logic in workflows (#35277) …

feat(Topology/Instances/EReal): limsup of multiplication by a constant (#35272) …

feat: lemmas for the analytic part of the proof of the Gelfond–Schneider theorem (Part 3/5) (#35315)

ci: Move GitHub apps private keys to Azure Key Vault and mint tokens Key Vault signing (#36150) …

chore: fix induction and recursor names (#35884) …

chore: remove unnecessary private and backward.privateInPublic (#36430) …

feat(Topology/Compactness/CompactSystem): introduce compact Systems (#36013) …

feat: add dist_center_midpoint_lt_radius for spheres (#35957) …

feat(Manifold/VectorBundle): tensoriality construction (#36432) …

feat(Data/Finsupp): characterise when `Finsupp` is `Nontrivial` (#35764) …

fix(Data/Rel): change what `image_eq_cod_of_dom_subset` states (#35696) …

feat(CategoryTheory/Limits/Preserves/Shapes/Kernels): Mapping `zeroKernelFork` (#36410) …

feat(RingTheory): add the class `HasFiniteQuotients` (#35530) …

chore: bump toolchain to v4.29.0-rc6 (#36422)

feat(Geometry/Euclidean): the Euclidean volume measure (#34697) …

chore: remove obsolete set_option backward.* (#36424) …

feat: properties of the real and imaginary parts in a complex star module (#36408) …

feat(Algebra): add two lemmas about submodule smul (#35646) …

chore(Computability): move TM files to a single folder (#35608) …