English
Let A be a seminormed commutative group, a ∈ A, and n ∈ ℕ. If orderOf(a) and n are coprime, then the action by a maps the approximate-order set with index n into the approximate-order set with index orderOf(a)·n (keeping the same δ).
Русский
Пусть A — полугруппа с нормой, a ∈ A, и n ∈ ℕ. Если orderOf(a) и n взаимно просты, то действие умножения на a переводит множество приближений порядка n в множество приближений порядка orderOf(a)·n (с тем же δ).
LaTeX
$$$$ a \\cdot \\operatorname{approxOrderOf}(A, n, \\delta) \\subseteq \\operatorname{approxOrderOf}(A, \\operatorname{orderOf}(a) \\cdot n, \\delta). $$$$
Lean4
@[to_additive]
theorem smul_subset_of_coprime (han : (orderOf a).Coprime n) :
a • approxOrderOf A n δ ⊆ approxOrderOf A (orderOf a * n) δ :=
by
simp_rw [approxOrderOf, thickening_eq_biUnion_ball, ← image_smul, image_iUnion₂, image_smul, smul_ball'', smul_eq_mul,
mem_setOf_eq]
refine iUnion₂_subset_iff.mpr fun b hb c hc => ?_
simp only [mem_iUnion, exists_prop]
refine ⟨a * b, ?_, hc⟩
rw [← hb] at han ⊢
exact (Commute.all a b).orderOf_mul_eq_mul_orderOf_of_coprime han
