English
Restricting a multiplicative equivalence between unit-root groups to nth roots of unity yields a canonical multiplicative equivalence between the corresponding root subgroups.
Русский
Ограничение мультиэквивалента между группами корней единицы до порядка n даёт каноническое мультипликативное эквивалент между соответствующими подгруппами корней единицы.
LaTeX
$$$\text{MulEquiv }(\operatorname{rootsOfUnity}_n(R) \to^* \operatorname{rootsOfUnity}_n(S))$$$
Lean4
/-- Restrict a monoid isomorphism to the nth roots of unity. -/
nonrec def restrictRootsOfUnity (σ : R ≃* S) (n : ℕ) : rootsOfUnity n R ≃* rootsOfUnity n S
where
toFun := restrictRootsOfUnity σ n
invFun := restrictRootsOfUnity σ.symm n
left_inv ξ := by ext; exact σ.symm_apply_apply _
right_inv ξ := by ext; exact σ.apply_symm_apply _
map_mul' := (restrictRootsOfUnity _ n).map_mul
