Mathlib Changelog
v4
Changelog
About
Github
Theorem
Submonoid.mem_unitClosedBall
Modification history
2026-06-16 13:55
Mathlib/Analysis/Normed/Field/UnitBall.lean
feat: define the closed unit disc in the complex numbers (#40511) …
Added
Submonoid.mem_unitClosedBall
View on Github →