Changelog

chore: fix four `Submonoid` recursors (#27185) …

chore: import `rw??` into `Mathlib.Tactic.Common` (#27164) …

feat(NumberTheory/Padics/ValuativeRel): ValuativeRel ℚ_[p] (#27177) …

feat: solution to ODE is Lipschitz with respect to the initial condition (#26392) …

chore: generalise `FreeGroup.ext_hom` to monoids (#27140) …

feat(CategoryTheory/Adjunction): the right partial adjoint (#27168) …

feat(Data/Matrix): add `Matrix.vecCons_inj` (#26896) …

feat: Finset.max'_eq_iff (#27153) …

feat(CategoryTheory/Preadditive/Injective/Basic, CategoryTheory/Preadditive/Projective/Basic): injectivity/projectivity criterion (#27156) …

feat(Algebra/SkewMonoidAlgebra/Basic): multiplication and algebraic instances (#26933) …

feat(Algebra/Polynomial/AlgebraMap): add lemmas (#26666)

chore: golf Algebra/ using `simp`/`simp_all` (#27130)

feat: add Mathlib.RingTheory.DedekindDomain.Instances (#26070) …

feat: coin problem with two coins and prime ideals in ℕ (#27065) …

feat: `Finset.mem_filter_univ` (#27148) …

feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): bicategory-like lemmas for `CatCospanTransforms` (#26447) …

chore: remove whitespace (#26963) …

feat(Topology/GDelta/Basic): two basic lemmas about unions of meagre sets (#26979) …

chore: golf CategoryTheory/ using `grind` (#26691)

feat(CategoryTheory/Topos): subobject classifier without limits (#26556) …

fix(Topology/Covering): switch to standard definition (#24983) …

chore(Topology.MetricSpace.Lipschitz): stop depending on Topology.Algebra (#23498) …

feat: characterise membership in `SO(2)` (#27121) …

feat(Algebra/GroupWithZero/Range): MonoidWithZeroHom.(m)range_nontrivial (#27114) …

feat: semilinearize `LinearEquiv.conjRingEquiv` (#27104)

refactor(LinearAlgebra/LinearIndependent): generalize some `LinearIndepOn` theorems (#27096) …

doc(Algebra/Homology/Homotopy): add field docstrings to `HomotopyEquiv` (#27048) …

chore(Analysis/InnerProductSpace/Projection): deprecating `subtypeL ∘ orthogonalProjection` in favor of `starProjection` (#26877) …

chore: golf RingTheory/ using `grind` (#26698)

chore: golf LinearAlgebra/ using `grind` (#26685)

chore: golf GroupTheory/ using `grind` (#26681)

feat: equivalent condition for subgroups to be simple (#26552) …

feat(AlgebraicTopology): cylinder objects in model categories (#26171) …

feat(Aesop): Improve SetLike ruleset (#25961) …

chore: rename arguments to `Matrix.submatrix` (#24883) …

chore: golf AlgebraicGeometry/ using `grind` (#26695)

feat: add instance `CanonicallyOrderedAdd` for `Ordinal` (#27145)

chore(Algebra): replace CoeFun.coe with DFunLike.coe (#27146)

chore: replace `DFunLike` → `FunLike` if possible (#27144) …

chore(RingTheory/ValuationSubring): valuationSubring_integers (#27111) …

feat: Subtype.map_{eq,ne} (#27012)

feat(CategoryTheory): `inv (μ F X Y) = δ F X Y` (#27061) …

feat(LinearAlgebra/Finsupp/LinearCombination): add `Submodule.mem_span_finset'` (#27097) …

feat: `(vecMulVec _ _).rank ≤ 1` (#27075) …

refactor: deprecate `sSup_le_sSup_of_forall_exists_le` in `CompleteLattice` in favor of `sSup_le_sSup_of_isCofinalFor` (#27124) …

refactor(Analysis/Convex/Mul): generalize the domain of functions (#27002) …

feat(Mathlib/Order/PartialSups): add `PartialSups` composition lemma (#26848) …

feat(Data/ENNReal): Add `sub_lt_iff_lt_left` and similar lemmas (#26815) …

fix(Logic/Function/Basic): change precedence of uncurry prefix operator to max (#26742) …

feat: inequalities for `(P ↓∩ Q).encard` (#27093) …