English
If m > 0 and gcd(n, m) = 1, then the set {y^m : y ∈ approxOrderOf(A, n, δ)} is contained in approxOrderOf(A, n, m δ).
Русский
Если m > 0 и gcd(n, m) = 1, то множество {y^m | y ∈ approxOrderOf(A, n, δ)} вложено в approxOrderOf(A, n, m δ).
LaTeX
$$$$ (\{ y^{m} : y \in \operatorname{approxOrderOf}(A, n, δ) \}) \subseteq \operatorname{approxOrderOf}(A, n, m δ), \quad 0 < m, \gcd(n,m)=1. $$$$
Lean4
@[to_additive]
theorem image_pow_subset_of_coprime (hm : 0 < m) (hmn : n.Coprime m) :
(fun (y : A) => y ^ m) '' approxOrderOf A n δ ⊆ approxOrderOf A n (m * δ) :=
by
rintro - ⟨a, ha, rfl⟩
obtain ⟨b, hb, hab⟩ := mem_approxOrderOf_iff.mp ha
replace hb : b ^ m ∈ {u : A | orderOf u = n} := by rw [← hb] at hmn ⊢; exact hmn.orderOf_pow
apply ball_subset_thickening hb ((m : ℝ) • δ)
convert pow_mem_ball hm hab using 1
simp only [nsmul_eq_mul, Algebra.id.smul_eq_mul]
