Changelog

ci: fix concurrency group (#31032) …

feat(CategoryTheory/Limits): precomposition with final functors and ColimitType (#30779) …

feat(SetTheory): more API for HasCardinalLT (#30633) …

feat(Topology/Sheaves): the equivalence `Over U ≌ Opens U` for `U : Opens X` (#30415)

feat: relation-separated sets (#23920) …

Feat(Logic): basic properties of boolean negation (#31028) …

feat(CategoryTheory): κ-filtered categories are stable under products (#30634) …

feat(CategoryTheory): Guitart exact squares and Kan extensions (#30382) …

feat(CategoryTheory/ObjectProperty): closure of a property under certain limits (#29854) …

feat: add mfderiv_prod and mfderiv_prodMap (#29589) …

feat(CategoryTheory): strong generators (#29519) …

feat(AlgebraicTopology/SimplicialSet): pairings of non degenerate simplices, following Sean Moss (#28332) …

feat(Algebra/Homology): Ext modules (#27416) …

feat(AlgebraicTopology): the homotopy category functor preserves products (#25780) …

feat(Algebra): `SemimoduleCat`, category of modules over semiring (#31023) …

feat(Analysis/Calculus): Taylor series converges to function on whole ball (#26267) …

feat(Topology/Algebra/Order/Archimedean): subgroups cyclic iff discrete (#30471) …

feat(UniformSpace/Completion): add `UniformSpace.Completion.mapEquiv` (#30574) …

chore(CategoryTheory/EssentiallySmall): adding an instance (#30534) …

feat(Topology): infinite T2 spaces (#30661)

feat(Combinatorics/Enumerative/Bell.lean): define standard Bell number (#26790)

chore(1000.yaml): add Fourier's theorem (#29047) …

feat: Lipschitz function criterion for weak convergence of probability measures (#30742) …

chore(AlgebraicGeometry): make SheafOfModule.IsQuasicoherent an ObjectProperty and clean up of finiteness conditions (#30372) …

feat(RingTheory/Finiteness): a finite and finitely presented algebra is finitely presented (#29781) …

refactor(AlgebraicTopology): redefine the topological simplex using the convexity API (#28893) …

feat(RingTheory/DedekindDomain/AdicValuation): add eq_of_valuation_isEquiv_valuation (#30404)

feat(FractionRing): generalize instIsScalarTower_1 (#30787) …

feat: introduce covarianceBilin (#30324) …

chore(scripts): add flt-regular to the downstream repositories (#31002) …

chore: deprecate duplicate Set.dual_ordConnected_iff (#31000)

chore: deprecate duplicate Quotient{,Add}Group.kerLift_mk' (#30999) …

feat(ENNReal): equality from comparing with nnreals (#30721) …

fix(Tactic/FunProp): use correct trace class name (#30514)

feat(AlgebraicGeometry): generalise Proj and HomogeneousLocalization to graded rings (#30302) …

chore(Analysis/SpecialFunctions/Pow): deprecate `rpow_lt_rpow_of_exponent_neg` and `rpow_le_rpow_of_exponent_nonpos` (#28375)

feat(Localization): `r / m` in the localisation is regular iff `r` is (#30708) …

chore(NumberTheory): golf `inftyValuation.polynomial` (#30979)

chore(Data/Nat/Periodic): golf (#30970)

feat(RatFunc): scalar tower instance from R[X] (#30963) …

chore(Analysis/InnerProductSpace/Defs): generalize `InnerProductSpace.ofCore` to allow for pre-inner product space (#30945) …

feat(Order/Cover): empty_covBy_singleton (#30915)

chore(Computability/Language): deprecate some duplicate order lemmas (#30912)

chore(without_cdot): remove all uses of `without_cdot` (#30735) …

chore(Algebra/Ring): shortcut `IsDomain` instances for `Nat` and `Int` (#30713) …

chore: use `grw`, `gcongr` even more (#30632) …

chore: regression test for Set grind annotations (#30627) …

chore(Combinatorics/SetFamily/KruskalKatona): remove outdated comment (#30564) …

feat: `CoeFun` for `Lex` and `Colex` (#30481) …

feat(SimpleGraph): characterise when `SimpleGraph V` is a subsingleton/nontrivial (#30137) …