Namespace AddCircle 1 theorems
- Torsion points of ℚ/ℤ have denominator any multiple of the order
AddCircle.exists_eq_coe_div_of_nsmul_eq_zero_of_dvd0 below · cited by 1 · depth 27
AddCircle 1 theoremsAddCircle.exists_eq_coe_div_of_nsmul_eq_zero_of_dvd 0 below · cited by 1 · depth 27