Changelog

feat: replace `Finsupp.embDomain_apply` with more general lemma (#31929) …

feat(Analysis/Asymptotics): Variants of isBigO_mul_iff_isBigO_div (#32544) …

chore(RingTheory): generalize `Algebra.intNorm` (#32542) …

feat(Dynamics/PeriodicPts): some theorems for `Pi.map` in `Dynamics/PeriodicPts` analogous to those for `Prod.map` (#29530) …

feat(Topology): UniformContinuous version of uniform limit theorem (#32079) …

feat(Combinatorics/SimpleGraph): characterise containment of `completeBipartiteGraph` (#27602) …

feat(ModularForms): norm and trace maps (#32460) …

feat(RingTheory/Coprime/Lemmas): Add Int.isCoprime_gcdA/B (#32369) …

feat: ext criterion wrt Icc for measures (#32516) …

chore(CategoryTheory): remove use of `erw` in `ι_gluedIso_hom` (#32523)

feat(Combinatorics/SimpleGraph/Acyclic): every acyclic subgraph can be extended to a maximal one (#32041) …

chore(scripts): update nolints.json (#32524) …

chore(CategoryTheory/ConcreteCategory): remove use of `erw` (#32519)

chore(CategoryTheory/Idempotents): remove uses of `erw` (#32520)

chore(CategoryTheory/Limits): remove use of `erw` in `limit.pre_π` and `limit.post_π` (#32518)

feat(Geometry/Manifold): mdifferentiability of finset sums/prods (#32514) …

chore(CategoryTheory/Localization): remove use of `erw` in `homMap_apply` (#32511)

chore(Data/Num): remove use of `erw` in `ofNat'_one` (#32504)

chore(Algebra/Module/LinearMap): remove use of `erw` (#32489)

chore: dualize `WithBot` and `WithTop` using `to_dual` (#32488)

chore: delete `Units.mulDistribMulAction'` (#32430) …

feat(Algebra/Homology): miscellaneous lemmas (#32434) …

feat(RingTheory): improved linearity of `Derivation.compDer` (#32509) …

chore(CategoryTheory/Limits/Shapes): remove use of `erw` in `cokernel.isColimitCoconeZeroCocone` (#32502)

chore(CategoryTheory/Limits): remove use of `erw` in `colimit.ι_post` (#32490)

chore(CategoryTheory/WithTerminal): remove use of `erw` in `liftStar_lift_map` (#32487)

chore(CategoryTheory/Subobject): remove use of `erw` in `imageSubobjectIso_comp_image_map` (#32485)

feat(Data/List/Basic): `idxOf` lemmas (#31930)

chore(CategoryTheory/Limits/Shapes/Opposites): remove use of `erw` in `Fan.IsLimit.op` (#32505)

feat(Algebra/Polynomial/Basic): Add ofMultiset (#32496) …

feat(Analysis/Convex/StrictCombination): convex combinations in strictly convex sets and spaces (#31452) …

chore(Order/SuccPred/Basic): use `to_dual` (#32447) …

feat: `WithVal v` and `WithVal w` are isomorphic as uniform spaces when `v` and `w` are equivalent valuations (#30133)

feat(Algebra/Homology): extensions of bifunctors to complexes preserve homotopies (#32383) …

chore(Probability): deprecate `Independence.Kernel` (#32465)

feat(LinearAlgebra/Multilinear): constructing `MultilinearMap` over `DirectSum` (#32450) …

feat(Data/Finset/Empty): add `@[push]` tags for pushing negation (#32195) …

feat(push): `push` annotations for `Real.log` (#30039) …

fix(Condensed/Explicit): typo in docstring (#32478)

chore: remove finiteness from Order.Filter.Lift (#23411)

chore(Probability): split `Independence.Kernel` (#32327) …

feat(LinearAlgebra/AffineSpace/Independent): injectivity of spans of images (#31979) …

feat(AlgebraicTopology): horns in `Δ[2]` as pushouts (#31802) …

feat(Combinatorics/Additive): subset-sum definition and basic properties (#31689) …

chore(Tactic/Measurability): `fun_prop` lemmas for solving `MeasurableSet {x | ...}` goals (#31592) …

feat(Geometry/Euclidean/MongePoint): `reindex` lemmas (#31210) …

feat(RingTheory/Extension/Cotangent): basis of free cotangent space can be realized as a presentation (#31034) …

feat(Combinatorics): Glaisher's theorem (#30618) …

feat(CategoryTheory): locally presentable categories and strong generators (#30241) …

chore: make sure that `Nat.AtLeastTwo` instances are constructive (#32467) …