isRoot_cyclotomic_iff — Mathlib

English

In a char p domain, a nonzero μ is a root of cyclotomic(p^k · m) R if and only if μ is a primitive m-th root of unity.

Русский

В кольце характеристика p, μ ≠ 0 является корнем cyclotomic(p^k · m) если и только если μ — примитивный m-й корень единицы.

LaTeX

$$$$ (\\operatorname{cyclotomic}(p^k \\cdot m, R)).\\text{IsRoot}(\\mu) \\iff \\text{IsPrimitiveRoot}(\\mu, m). $$$$

Lean4

theorem isRoot_cyclotomic_iff [NeZero (n : R)] {μ : R} : IsRoot (cyclotomic n R) μ ↔ IsPrimitiveRoot μ n :=
  by
  have hf : Function.Injective _ := IsFractionRing.injective R (FractionRing R)
  haveI : NeZero (n : FractionRing R) := NeZero.nat_of_injective hf
  rw [← isRoot_map_iff hf, ← IsPrimitiveRoot.map_iff_of_injective hf, map_cyclotomic, ← isRoot_cyclotomic_iff']

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