zeta_spec — Mathlib

English

The element zeta defined in a cyclotomic extension is a primitive n-th root of unity.

Русский

Элемент ζ в циклотомическом расширении является примитивным корнем n-й степени единства.

LaTeX

$$$\text{IsPrimitiveRoot}(\zeta\, n\, A\, B)$$$

Lean4

/-- `zeta n A B` is a primitive `n`-th root of unity. -/
@[simp]
theorem zeta_spec : IsPrimitiveRoot (zeta n A B) n :=
  (exists_isPrimitiveRoot A B (Set.mem_singleton n) (NeZero.ne _) : ∃ r : B, IsPrimitiveRoot r n).choose_spec

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