Mathlib Changelog
Changelog
About
Github
Commit
2022-12-28 13:01
422e70f7
View on Github →
feat(topology/instances/add_circle): expand API for finite-order points on the circle (
#17986
)
Estimated changes
Modified
src/data/set/finite.lean
added
theorem
set.not_inj_on_infinite_finite_image
Modified
src/data/set/intervals/infinite.lean
modified
theorem
set.Ioi_infinite
Modified
src/group_theory/order_of_element.lean
added
theorem
infinite_not_is_of_fin_order
added
theorem
injective_pow_iff_not_is_of_fin_order
added
theorem
not_is_of_fin_order_of_injective_pow
Modified
src/topology/instances/add_circle.lean
added
theorem
add_circle.add_order_of_eq_pos_iff
added
theorem
add_circle.card_add_order_of_eq_totient
added
theorem
add_circle.coe_add
added
theorem
add_circle.coe_sub
added
theorem
add_circle.finite_set_of_add_order_eq
added
def
add_circle.set_add_order_of_equiv