Commit 2023-05-16 15:19 95a9188d

View on Github →

feat: port Analysis.Normed.Group.AddCircle (#4023)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Normed/Group/AddCircle.lean

added theorem AddCircle.closedBall_eq_univ_of_half_period_le

added theorem AddCircle.coe_real_preimage_closedBall_eq_iUnion

added theorem AddCircle.coe_real_preimage_closedBall_inter_eq

added theorem AddCircle.coe_real_preimage_closedBall_period_zero

added theorem AddCircle.exists_norm_eq_of_isOfFinAddOrder

added theorem AddCircle.le_add_order_smul_norm_of_isOfFinAddOrder

added theorem AddCircle.norm_coe_eq_abs_iff

added theorem AddCircle.norm_coe_mul

added theorem AddCircle.norm_div_nat_cast

added theorem AddCircle.norm_eq'

added theorem AddCircle.norm_eq

added theorem AddCircle.norm_eq_of_zero

added theorem AddCircle.norm_half_period_eq

added theorem AddCircle.norm_le_half_period

added theorem AddCircle.norm_neg_period

added theorem UnitAddCircle.norm_eq