Sync upstream mathlib4 (2026-05-11, +30 commits)#5

Merged

winstonyin-ax merged 31 commits into

May 11, 2026

Commits on May 11, 2026

feat(GroupTheory/Torsion): torsion subgroup of a product (#38729)
tb65536
committed
chore(Condensed/Light/Epi): remove an erw (#38768)

yuanyi-350
and
dagurtomas
committed
refactor(NumberTheory): golf `Mathlib/NumberTheory/FrobeniusNumber` (#38832)
yuanyi-350
committed
refactor(NumberTheory): golf `Mathlib/NumberTheory/EllipticDivisibilitySequence` (#38833)
yuanyi-350
committed
feat(RingTheory.DedekindDomain.Factorization): add API for factorization (#38654)
MichaelStollBayreuth
committed
chore(NumberTheory/Height/NumberField): move positivity extension higher up (#39181)
MichaelStollBayreuth
committed
feat(Algebra/Homology): homology sequence and acyclic complexes (#38999)
joelriou
committed
chore(Geometry): move `ConvexSpace` out of `LinearAlgebra` (#38907)
YaelDillies
committed
chore(FinitelyPresentedGroup): Use dot notation by default whenever possible and typo fix (#38971)
homeowmorphism
committed
feat: normal function has a closed range (#39137)
vihdzp
committed
feat(CategoryTheory): characterize pullback squares via the `Over` category (#36216)
michaellee94
committed
chore: golf `Cardinal.isRegular_succ` (#36930)
vihdzp
committed
feat(Category/Kernel): `Stoch` is a positive Markov category (#37851)
gaetanserre
committed
chore(MeasureTheory): replace remaining `@[measurability]` attributes by `@[fun_prop]` (#38512)
gasparattila
committed
refactor(NumberTheory): golf `Mathlib/NumberTheory/Zsqrtd/GaussianInt` (#38835)
yuanyi-350
committed
chore(ModelTheory/ElementaryMaps): remove an erw (#38925)
yuanyi-350
committed
feat(AlgebraicGeometry/Restrict): strengthen a technical lemma (#39142)
justus-springer
committed
feat: generalize `isOpen_iff_dirSupInacc` (#37307)
vihdzp
committed
chore(Logic/Function/Basic): avoid defeq abuse of `Set α = α → Prop` in Cantor's theorem (#39147)
SnirBroshi
committed
feat(CategoryTheory/Localization): derivability structures and Guitart exact squares (#39028)
joelriou
committed
chore: rename two instances (#38208)
mbkybky
committed
feat: add more API for (rel)index and ideals (#39118)
MichaelStollBayreuth
committed
feat(Analysis/Convex/Segment): add lineMap_mem_segment (#39198)
FordUniver
committed
refactor(LinearAlgebra/Projection): refactor `quotientEquivOfIsCompl` via `LinearEquiv.ofLinear` (#38814)
sharky564
committed
feat(SheafCohomology): add API for Sheaf Cohomology (#34742)
Brian-Nugent
committed
feat: lower bounds for Chebyshev theta and psi functions (#38986)
teorth
committed
feat(Algebra/Homology): the homotopy category of bounded below cochain complexes (#39076)

joelriou
and
pre-commit-ci-lite[bot]
committed
feat(Algebra/Module): a finite stably free module `M` is free if it is invertible (#37216)

mbkybky
and
pre-commit-ci-lite[bot]
committed
feat(RingTheory/Unramified/Locus): add `iff` lemma relating `Unramified` to `IsUnramifiedAt` (#39072)
tb65536
committed
feat(RingTheory/RamificationInertia/Inertia): add `inertiaDeg'_pos` (#39073)
tb65536
committed
Merge upstream/master@686c76b39d (2026-05-11)
github-actions[bot]
committed