exists_prim_root — Mathlib

English

Assuming IsCyclotomicExtension, for any n in S, there exists an element r in B that is a primitive n-th root of unity.

Русский

Пусть IsCyclotomicExtension; для любого n ∈ S существует элемент r в B, являющийся примитивным корнем единицы степени n.

LaTeX

$$∃ r ∈ B, IsPrimitiveRoot r n$$

Lean4

@[deprecated exists_isPrimitiveRoot (since := "2025-05-21")]
theorem exists_prim_root [IsCyclotomicExtension S A B] {n : ℕ} (ha : n ∈ S) (ha' : n ≠ 0) :
    ∃ r : B, IsPrimitiveRoot r n :=
  exists_isPrimitiveRoot A B ha ha'

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