Mathlib Changelog
Changelog
About
Github
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