of_dvd — Mathlib

English

If HasEnoughRootsOfUnity M n and m divides n, then HasEnoughRootsOfUnity M m.

Русский

Если M имеет HasEnoughRootsOfUnity для n и m делит n, тогда имеют HasEnoughRootsOfUnity для m.

LaTeX

$$HasEnoughRootsOfUnity.of_dvd: m ∣ n → HasEnoughRootsOfUnity M n → HasEnoughRootsOfUnity M m$$

Lean4

/-- If `HasEnoughRootsOfUnity M n` and `m ∣ n`, then also `HasEnoughRootsOfUnity M m`. -/
theorem of_dvd (M : Type*) [CommMonoid M] {m n : ℕ} [NeZero n] (hmn : m ∣ n) [HasEnoughRootsOfUnity M n] :
    HasEnoughRootsOfUnity M m
    where
  prim :=
    have ⟨ζ, hζ⟩ := exists_primitiveRoot M n
    have ⟨k, hk⟩ := hmn
    ⟨ζ ^ k, IsPrimitiveRoot.pow (NeZero.pos n) hζ (mul_comm m k ▸ hk)⟩
  cyc := Subgroup.isCyclic_of_le <| rootsOfUnity_le_of_dvd hmn

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