English
There is an equivalence between the group of nth roots of unity in a domain R and the set of nth roots of 1 in R, via the unit-group viewpoint.
Русский
Существует эквиваленция между корнями единицы порядка n в окружении R и множеством n-ой корней 1 в R через группу единиц.
LaTeX
$$$\operatorname{rootsOfUnity}_n(R) \simeq { x \mid x \in \operatorname{nthRoots}_n(1) }$$$
Lean4
/-- Equivalence between the `k`-th roots of unity in `R` and the `k`-th roots of `1`.
This is implemented as equivalence of subtypes,
because `rootsOfUnity` is a subgroup of the group of units,
whereas `nthRoots` is a multiset. -/
def rootsOfUnityEquivNthRoots : rootsOfUnity k R ≃ { x // x ∈ nthRoots k (1 : R) }
where
toFun x := ⟨(x : Rˣ), mem_rootsOfUnity_iff_mem_nthRoots.mp x.2⟩
invFun
x := by
refine ⟨⟨x, ↑x ^ (k - 1 : ℕ), ?_, ?_⟩, ?_⟩
all_goals
rcases x with ⟨x, hx⟩; rw [mem_nthRoots <| NeZero.pos k] at hx
simp only [← pow_succ, ← pow_succ', hx, tsub_add_cancel_of_le NeZero.one_le]
simp only [mem_rootsOfUnity, Units.ext_iff, Units.val_pow_eq_pow_val, hx, Units.val_one]
