toRootsOfUnity — Mathlib

English

Turn a primitive root μ into a member of the rootsOfUnity subgroup.

Русский

Преобразовать примитивный корень μ в элемент подгруппы rootsOfUnity.

LaTeX

$$$\mathrm{toRootsOfUnity}(\mu,n,h) \in \mathrm{rootsOfUnity}_{n} M$$$

Lean4

/-- Turn a primitive root μ into a member of the `rootsOfUnity` subgroup. -/
@[simps!]
def toRootsOfUnity {μ : M} {n : ℕ} [NeZero n] (h : IsPrimitiveRoot μ n) : rootsOfUnity n M :=
  rootsOfUnity.mkOfPowEq μ h.pow_eq_one

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