Changelog

feat(Combinatorics/Additive/VerySmallDoubling): Hamidoune's Freiman-Kneser theorem for nonabelian groups (#28296) …

feat(CategoryTheory/Sites): more API for zero hypercovers (#30906) …

feat(AlgebraicGeometry/Morphisms/Flat): add a simple lemma (#30237) …

chore(CategoryTheory/Sites/Precoverage): remove universe parameters in `IsStableUnderBaseChange` etc. (#30835) …

chore: rephrase leOnePart_le_one/negPart_nonpos (#30899) …

chore: remove duplicate `Ordinal.deriv_id_of_nfp_id` (#30893)

chore: deprecate duplicate Rat.{nat,int}Cast_eq_zero and rename _eq_one lemmas (#30868)

feat(RingTheory): Noetherian ring of fractions is semilocal (#30837) …

chore(Data/ENNReal): deprecate duplicate `sup_eq_zero` (#30883) …

feat(AlgebraicGeometry): quasi-affine if covered by affine basic opens of global sections (#30286)

chore(Data/Fintype/Sets): deprecate duplicate `toFinset_subset_toFinset_of_subset` (#30884) …

feat(CategoryTheory/Adjunction/PartialAdjunction): add symm naturality lemmas for HomEquiv and lift functor (#30143) …

chore: don't push oleans to Cloudflare (#30875) …

feat(CategoryTheory/Limits/Shapes): (co)kernel as a functor (#30674) …

feat(Algebra/BigOperators/Finsupp/Fin): add finTwoArrowEquiv (#30538) …

chore: bump leantar to v0.1.16 (#30874)

chore: deprecate duplicate Polynomial.monic_of_degree_le_of_coeff_eq_one (#30865)

Fix: change how multigoal linter handles focus. (#30470) …

chore: drop duplicate instance Rat.hasSolidNorm (#30864) …

feat: if the order topology for a dense linear ordering is discrete, the space has at most one point (#30856) …

feat(Combinatorics/SimpleGraph): inducing a walk (#30590) …

feat(CategoryTheory): LeftBousfield.W is stable under transfinite compositions (#30509)

fix: make Set.Subsingleton.offDiag_eq_empty match its name (#30863)

refactor(Algebra/Polynomial/Splits): switch from `Splits` to `Factors` (#30284)

chore: deprecate Nat.factorization_eq_zero_of_non_prime (#30862)

feat(GroupTheory/Finiteness): submonoid finiteness from well-quasi-order, Gordan's lemma (#30840) …

feat: `isProperMap_fst_of_compactSpace`, `IsProperMap.restrictPreimage` (#30410)

feat(Topology): the topology generated by a family of spaces (#29341) …

refactor(Topology/UniformSpace): use `SetRel` (#23181) …

feat(RingTheory/IsTensorProduct): add `IsPushout.cancelBaseChange` (#28772) …

chore(Data): `SetLike Finset` (#28241)

chore(GroupTheory/Index): move awkwardly placed lemmas (#30832) …

feat(Data/Finset/Card): add some more Pigeonhole Principle theorems `exists_ne_map_eq_of_card_image_lt` and `not_injOn_of_card_image_lt` (#28077) …

feat(DedekindDomain): formulas for the different ideal in the compositum of disjoint extensions (#29770) …

chore: LEAN_SRC_PATH for reap (#30839) …

feat(FieldTheory): construct extension of finite field (#30738) …

chore: do not double-build nightly-testing non-fork PRs (#30834) …

feat: convexOn_rpow_left (#30829)

feat: add `ContinuousSMul` instances for `ℚ≥0` (#28474)

feat: enorm_div_rev (#30830)

feat(Algebra/Star): define the intrinsic star on linear maps (#29941) …

feat: interplay of posPart, negPart, untop₀, min and max (#30774) …

chore: remove more instance fields (#30753) …

feat(Data/Set/Pairwise): prove pairwise results for Chains, move `Set.pairwise_iUnion₂` (#28119) …

feat: sharp bounds for `‖exp (I * x) - 1‖` when `x` is real (#27252) …

style(Data): fix whitespace (#30778) …

feat(Order/WellFoundedSet): `partiallyWellOrderedOn_univ_iff` and `Pi.wellQuasiOrderedLE` (#30275) …

feat: properties of sesquilinear forms over a star ring (#30274)

refactor: make `PosMulMono` and alike custom classes (#29395) …

feat(GroupTheory/FreeGroup/Orbit): The orbit of a point generated by parts of a free group can be "duplicated" (#30130) …