exists_primitiveRoot — Mathlib

English

If M is a commutative monoid with HasEnoughRootsOfUnity for n, there exists an element ζ with IsPrimitiveRoot ζ n.

Русский

Если M — коммутативный моноид с HasEnoughRootsOfUnity для n, существует элемент ζ с IsPrimitiveRoot ζ n.

LaTeX

$$HasEnoughRootsOfUnity.exists_primitiveRoot: exists ζ ∈ M, IsPrimitiveRoot ζ n$$

Lean4

theorem exists_primitiveRoot (M : Type*) [CommMonoid M] (n : ℕ) [HasEnoughRootsOfUnity M n] :
    ∃ ζ : M, IsPrimitiveRoot ζ n :=
  HasEnoughRootsOfUnity.prim

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