isCyclic — Mathlib

English

The restricted map respects the underlying monoid-homomorphism-coe correspondence.

Русский

Ограниченное отображение согласуется с образцом коe и соответствием моноид-гомоморфизма.

LaTeX

$$$(\restrictRootsOfUnity \sigma k\ ζ) = σ(ζ)$$$

Lean4

instance isCyclic : IsCyclic (rootsOfUnity k R) :=
  isCyclic_of_subgroup_isDomain ((Units.coeHom R).comp (rootsOfUnity k R).subtype) coe_injective

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