mem_rootsOfUnity' — Mathlib

English

From a unit ζ in M and a positive n with ζ^n = 1, we obtain an element of rootsOfUnity n M.

Русский

Из единицы ζ в M и положительного n с ζ^n = 1 получаем элемент rootsOfUnity n M.

LaTeX

$$$\text{If } \zeta^n = 1,\ n>0, \text{ then } \text{mkOfPowEq}(\zeta,n,h) \in \mathrm{rootsOfUnity}(n,M).$$$

Lean4

/-- A variant of `mem_rootsOfUnity` using `ζ : Mˣ`. -/
theorem mem_rootsOfUnity' (k : ℕ) (ζ : Mˣ) : ζ ∈ rootsOfUnity k M ↔ (ζ : M) ^ k = 1 := by rw [mem_rootsOfUnity];
  norm_cast

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