Commit 2022-11-22 09:37 084f76e2

View on Github →

feat(analysis/normed/group/add_circle): results about finite-order points on the circle (#17321) The main motivation for developing this API is the lemma add_circle.le_add_order_smul_norm_of_is_of_fin_add_order

Estimated changes

Modified src/algebra/order/floor.lean

added theorem abs_sub_round_div_nat_cast_eq

added theorem int.fract_div_int_cast_eq_div_int_cast_mod

added theorem int.fract_div_nat_cast_eq_div_nat_cast_mod

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

added theorem add_circle.exists_norm_eq_of_fin_add_order

added theorem add_circle.le_add_order_smul_norm_of_is_of_fin_add_order

added theorem add_circle.norm_div_nat_cast

added theorem add_circle.norm_eq'

Modified src/data/nat/cast/field.lean

added theorem nat.cast_div_div_div_cancel_right

Modified src/group_theory/subgroup/basic.lean

added theorem subgroup.npow_mem_zpowers

Modified src/topology/instances/add_circle.lean

added theorem add_circle.add_order_of_coe_rat

added theorem add_circle.add_order_of_div_of_gcd_eq_one'

added theorem add_circle.add_order_of_div_of_gcd_eq_one

added theorem add_circle.coe_eq_zero_iff

added theorem add_circle.coe_eq_zero_of_pos_iff

added theorem add_circle.exists_gcd_eq_one_of_is_of_fin_add_order

added theorem add_circle.gcd_mul_add_order_of_div_eq