smul_eq_of_mul_dvd — Mathlib

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) δ

Похожие утверждения