English
Let hn > 0 and han be that orderOf(a)^2 divides n. Then multiplying by a preserves the approximate-order set with index n: a • approxOrderOf(A, n, δ) = approxOrderOf(A, n, δ).
Русский
Пусть hn > 0 и ha n.d., что orderOf(a)^2 делит n. Тогда умножение на a сохраняет множество приближений порядка n: a • approxOrderOf(A, n, δ) = approxOrderOf(A, n, δ).
LaTeX
$$$$ a \\cdot \\operatorname{approxOrderOf}(A, n, δ) = \\operatorname{approxOrderOf}(A, n, δ) $$$$
Lean4
@[to_additive vadd_eq_of_mul_dvd]
theorem smul_eq_of_mul_dvd (hn : 0 < n) (han : orderOf a ^ 2 ∣ n) : a • approxOrderOf A n δ = approxOrderOf A n δ :=
by
simp_rw [approxOrderOf, thickening_eq_biUnion_ball, ← image_smul, image_iUnion₂, image_smul, smul_ball'', smul_eq_mul,
mem_setOf_eq]
replace han : ∀ {b : A}, orderOf b = n → orderOf (a * b) = n :=
by
intro b hb
rw [← hb] at han hn
rw [sq] at han
rwa [(Commute.all a b).orderOf_mul_eq_right_of_forall_prime_mul_dvd (orderOf_pos_iff.mp hn) fun p _ hp' =>
dvd_trans (mul_dvd_mul_right hp' <| orderOf a) han]
let f : {b : A | orderOf b = n} → {b : A | orderOf b = n} := fun b => ⟨a * b, han b.property⟩
have hf : Surjective f := by
rintro ⟨b, hb⟩
refine ⟨⟨a⁻¹ * b, ?_⟩, ?_⟩
· rw [mem_setOf_eq, ← orderOf_inv, mul_inv_rev, inv_inv, mul_comm]
apply han
simpa
· simp only [f, mul_inv_cancel_left]
simpa only [mem_setOf_eq, Subtype.coe_mk, iUnion_coe_set] using hf.iUnion_comp fun b => ball (b : A) δ