English
An element a ∈ 𝕜 represents a point in AddCircle(p) that does not have finite order exactly when, for every rational q, q does not equal a/p in 𝕜.
Русский
Элемент a ∈ 𝕜 имеет бесконечный порядок в AddCircle(p) тогда и только тогда, когда для всякого рационального числа q выполняется q ≠ a/p в 𝕜.
LaTeX
$$$\neg IsOfFinAddOrder(a) \iff \forall q \in \mathbb{Q}, q \neq a/p$$$
Lean4
instance : DivisibleBy (AddCircle p) ℤ
where
div x n := (↑((n : 𝕜)⁻¹ * (equivIco p 0 x : 𝕜)) : AddCircle p)
div_zero x := by simp
div_cancel {n} x
hn := by
replace hn : (n : 𝕜) ≠ 0 := by norm_cast
change n • QuotientAddGroup.mk' _ ((n : 𝕜)⁻¹ * ↑(equivIco p 0 x)) = x
rw [← map_zsmul, ← smul_mul_assoc, zsmul_eq_mul, mul_inv_cancel₀ hn, one_mul]
exact (equivIco p 0).symm_apply_apply x
