Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-03 06:36 ebe6bda5

View on Github →

feat(analysis/normed/group/add_circle): define the additive circle (#16201)

Estimated changes

Modified src/algebra/order/archimedean.lean

deleted theorem floor_ring.archimedean

Modified src/algebra/order/to_interval_mod.lean

added theorem to_Ico_mod_eq_fract_mul

added theorem to_Ico_mod_mem_Ico'

Created src/analysis/normed/group/add_circle.lean

added theorem add_circle.norm_coe_mul

added theorem add_circle.norm_eq

added theorem add_circle.norm_eq_of_zero

added theorem unit_add_circle.norm_eq

Modified src/analysis/normed/group/quotient.lean

added theorem add_subgroup.quotient_norm_eq

Modified src/analysis/special_functions/trigonometric/angle.lean

modified def real.angle

Modified src/group_theory/subgroup/basic.lean

added theorem add_subgroup.int_cast_mem_zmultiples_one

added theorem add_subgroup.int_cast_mul_mem_zmultiples

added theorem subgroup.zpow_mem_zpowers

Created src/topology/instances/add_circle.lean

added theorem add_circle.coe_equiv_Ico_mk_apply

added theorem add_circle.coe_image_Icc_eq

added theorem add_circle.compact_space

added theorem add_circle.continuous_equiv_Ico_symm

added def add_circle.equiv_Ico

added def add_circle.equiv_add_circle

added theorem add_circle.equiv_add_circle_apply_mk

added theorem add_circle.equiv_add_circle_symm_apply_mk

added def add_circle

added def unit_add_circle