Sync upstream mathlib4 (2026-08-01, +14 commits) - #91

Merged

winstonyin-ax merged 15 commits into

Aug 1, 2026

Commits on Jul 31, 2026

chore(CategoryTheory): remove `backward` options using `implicit_reducible` (#42161)
JovanGerb
committed
0f0a217
feat(Algebra/QuadraticAlgebra): add the trace (#42207)
xroblot
committed
ca6d69c
chore(Translate/ToDual): remove redundant entry from `abbreviationDict` (#42251)
JovanGerb
committed
d1906c8
chore(Analysis/Seminorm): generalize typeclasses slightly (#42300)
mcdoll
committed
b2933a1
chore(GroupTheory): fix non-terminal simp (#42302)
yuanyi-350
committed
6ecc792
fix(Translate): support structures where a universe level doesn't appear in the type (#42228)
JovanGerb
committed
232b5fd
perf(AlgebraicGeometry/Group/Affine): specify the universe explicitly (#42303)
JovanGerb
committed
45e3065
feat(RepresentationTheory): add a surjectivity lemma for irreducible representations (#42151)
JX-Mo
committed
6a58949
perf(MeasureTheory/Integral/IntervalIntegral/Periodic): explicit proof instead of aesop (#41870)
FawadHa1der
committed
a366f87
feat (Linter/Header): add config for custom copyright (#41876)
oliver-butterley
committed
ff4f94a
chore(FGModuleCat/EssentiallySmall): generalize to `Ring` (#42006)
ybenmeur
committed
d222514
feat(LinearAlgebra): use `IsApply` for `QuadraticMap` (#42134)
mcdoll
committed
ce88332
chore(RingTheory/*): remove domain assumptions by generalizing from torsion free to faithful smul (#41379)
tb65536
committed
f4570dc
fix: adaptations for batteries #1927 (#42229)

wrenna-robson
and
mathlib-nightly-testing[bot]
committed
1f8806b

Commits on Aug 1, 2026

Merge upstream/master@1f8806b67d (2026-08-01)
github-actions[bot]
committed
4ea40cd