Commit 2023-03-14 00:02 d81c6ecd

View on Github →

feat: port Analysis.Normed.Field.UnitBall (#2857)

Estimated changes

Modified Mathlib.lean

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

added def Submonoid.unitClosedBall

added def Submonoid.unitSphere

added def Subsemigroup.unitBall

added def Subsemigroup.unitClosedBall

added theorem coe_div_unitSphere

added theorem coe_inv_unitSphere

added theorem coe_mul_unitBall

added theorem coe_mul_unitClosedBall

added theorem coe_mul_unitSphere

added theorem coe_one_unitClosedBall

added theorem coe_one_unitSphere

added theorem coe_pow_unitClosedBall

added theorem coe_pow_unitSphere

added theorem coe_zpow_unitSphere

added def unitSphereToUnits

added theorem unitSphereToUnits_apply_coe

added theorem unitSphereToUnits_injective