Changelog

feat: `casesm` tactic reuses hypothesis name if only one new hypothesis (#20763) …

fix: make `NNRatCast` computable for `NNReal` and `ENNReal` (#20884) …

feat: show `IsGreatest (spectrum ℝ≥0 a) ‖a‖₊` for `IsometricContinuousFunctionalCalculus` (#20882) …

feat: tag `csInf_insert` and `csSup_insert` `@[simp]` (#20883) …

refactor(LinearAlgebra/Projection): Use IsIdempotentElem (#20665) …

chore: replace open scoped Classical with `open scoped Classical in` or `classical` (#20501) …

feat(Logic/Basic): `HEq (cast h a) b ↔ HEq a b` (#20847) …

feat(Data/Matroid/Basic): matroid congruence definitions (#20876) …

feat: `notation3`-defined pretty printers now make tokens that are clickable in documentation (#20861) …

feat(GroupTheory/SpecificGroups): dihedral groups are not cyclic (with one exception) (#20817)

fix(Linter/Style.lean): fix some outdated comments (#20879)

chore(100,1000.yaml): name the authors field 'authors' (#20875) …

doc(Order/KrullDimension): clarify docstring of height, coheight (#20868)

chore: rename ENNReal lemmas to mul_{left,right}_inj for consistency (#20880)

feat(Data/Matroid/IndepAxioms): Another constructor for finitary matroids (#20877) …

style: replace `field x y := match x, y with` with `field` (#20866) …

feat(Order/Chain): adapt linear order lemmas to chains (#20757) …

feat(CategoryTheory/Localization): HasLocalization holds iff the localized category is locally small (#20670) …

feat(AlgebraicGeometry): Formally unramified morphisms (#20603)

feat(AlgebraicGeometry): Instances regarding affine spaces (#20314)

feat(Analysis/Pow/Deriv): add some results about differentiability of cpow (#19944) …

feat(Data/Matroid/Restrict): added a few matroid restriction lemmas (#19838) …

feat: use to_additive for Monoid.End (#19687) …

feat(RingTheory/Trace): the trace from a ring `R` to itself is the identity (#20865) …

chore(Algebra/CharP): `prime_ringChar` and `isPrimePow_card` (#20860) …

feat(RingTheory/Invariant): Galois extensions satisfy `Algebra.IsInvariant` (#20106) …

feat: the pairs `{t, insert a t}` are pairwise disjoint (#20062) …

feat: Myhill–Nerode theorem (#11311) …

feat(RingTheory): minimal primes are contained in zero divisors (#20306)

chore(Data/Matroid/Basic): a few tweaks to `Matroid.Basic` (#19836) …

chore(LinearAlgebra): generalize results on ranks to semirings (#20774)

feat(CategoryTheory): localization of trifunctors (#20788) …

feat(RingTheory/Idempotents): generalize to Semiring, add Corner and direct product decomposition (#20531) …

refactor(RingTheory): split off heavy results from `Mathlib/RingTheory/Spectrum/*/Basic.lean` (#20845) …

feat: add lemmas for working with orders of analytic functions (#20813) …

feat(RingTheory): `H¹(L)` under localization (#20591)

chore(Order): split `GaloisConnection` into `Defs.lean` and `Basic.lean` (#20798) …

feat(BigOperators): ite_prod_one / ite_sum_zero (#20779) …

feat(RingTheory): prime is restriction of a prime iff it is the restriction of its extension (#20700) …

feat(RingTheory/Ideal): the height of an ideal (#20741) …

feat(Algebra/Category/Grp/LargeColimits): large colimits in the category of commutative additive groups (#20522) …

feat: more `PGame.identical` `PGame.memₗ` `PGame.memᵣ` APIs (#5901) …

feat: make `Sub ℝ≥0` and `Sub ℝ≥0∞` computable (#20856) …

feat: restriction of scalars for root pairings with coefficients in a field (#20384) …

feat(SetTheory/Order/Basic): not_lt_iff_not_le_or_ge (#19973) …

doc(MeasurableSpace/CountablyGenerated): fix declaration names in module doc (#20863) …

feat: inequalities on complex exponentials (#20844) …

chore(Algebra/Order/Floor): Split off `round` section (#20831) …

feat: `Pi.ofNat_def` (#20857)

feat(Order/OrderIsoNat): sequence in well-founded order is not `StrictAnti` (#20851)