Commit 2025-03-28 11:58 d89d09f0

View on Github →

feat(Analysis/Normed): generalize unit ball results (#23378) The unit sphere is a monoid, over any normed ring satisfying NormMulClass. Etc.

Estimated changes

Modified Mathlib/Analysis/Normed/Field/UnitBall.lean

modified def Submonoid.unitSphere

modified theorem coe_mul_unitSphere

modified theorem coe_one_unitSphere

modified theorem coe_pow_unitSphere