rootsOfUnityEquivNthRoots_apply — Mathlib

English

Applying the nthRoots equivalence and then taking the image under the inverse map yields the identity on the corresponding elements.

Русский

Применение эквивалентности корней единицы и взятие образа через обратное отображение сводит к тождественному отображению.

LaTeX

$$$(rootsOfUnityEquivNthRoots\;R\;k).symm = (\text{inverse})$$$

Lean4

@[simp]
theorem rootsOfUnityEquivNthRoots_apply (x : rootsOfUnity k R) :
    (rootsOfUnityEquivNthRoots R k x : R) = ((x : Rˣ) : R) :=
  rfl

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