rootsOfUnityEquivOfPrimitiveRoots

Lean4
/-- If `R` contains an `n`-th primitive root, and `S/R` is a ring extension,
then the `n`-th roots of unity in `R` and `S` are isomorphic.
Also see `IsPrimitiveRoot.map_rootsOfUnity` for the equality as `Subgroup Sˣ`. -/
@[simps! -isSimp apply_coe_val apply_coe_inv_val]
noncomputable def _root_.rootsOfUnityEquivOfPrimitiveRoots {S F} [CommRing S] [IsDomain S] [FunLike F R S]
    [MonoidHomClass F R S] {n : ℕ} [NeZero n] {f : F} (hf : Function.Injective f) (hζ : (primitiveRoots n R).Nonempty) :
    (rootsOfUnity n R) ≃* rootsOfUnity n S :=
  (Subgroup.equivMapOfInjective _ (Units.map f) (Units.map_injective hf)).trans
    (MulEquiv.subgroupCongr <| ((mem_primitiveRoots <| NeZero.pos n).mp hζ.choose_spec).map_rootsOfUnity hf)
Похожие утверждения