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

Merged

winstonyin-ax merged 12 commits into

May 11, 2026

Commits on May 10, 2026

feat(Analysis/CStarAlgebra/Spectrum): Adding lemmas that the CStarAlgebra norm equals the square root of the spectral radius of star a * a (#33178)

gw90
and
j-loreaux
committed
feat: integrability of terms in Cartan's formula (#38581)
kebekus
committed
feat: variants of the principle of isolated zeros for meromorphic functions (#38984)
kebekus
committed
feat(SetTheory): ℵ_ univ = univ (#37545)
vihdzp
committed
chore: fix name of theorem in docstring (#39148)
vihdzp
committed
feat: add IsMulCommutative instances for directed families of commutative subobjects (#36553)
j-loreaux
committed
feat(SetTheory/Ordinal/Exponential): characterization of `a ^ b = 1` (#36891)

vihdzp
and
plp127
committed
feat: `Order.cof Ordinal = univ` (#37675)
vihdzp
committed
feat(Algebra/Order): stronger positivity criterion for `expect` (#38794)
YaelDillies
committed
refactor(Topology/Algebra/Module/LinearMap): rename subtypeL companion lemmas (#38962)
sharky564
committed
feat: generalize Submodule.ClosedComplemented.of_quotient_finiteDimensional (#38579)
ADedecker
committed

Commits on May 11, 2026

Merge upstream/master@50f0559af9 (2026-05-11)
github-actions[bot]
committed