English
If g generates G and g' in G' has order dividing order of g, there exists a homomorphism G →* G' mapping g to g'.
Русский
Если g порождает G и элемент g' в G' имеет порядок, делимый порядком g, существует гомоморфизм G →* G', переводящий g в g'.
LaTeX
$$∃ monoidHom f : G →* G' with f(g)=g' whenever g generates G and order(g') | order(g)$$
Lean4
/-- If `g` generates the group `G` and `g'` is an element of another group `G'` whose order
divides that of `g`, then there is a homomorphism `G →* G'` mapping `g` to `g'`. -/
@[to_additive /-- If `g` generates the additive group `G` and `g'` is an element of another additive group `G'`
whose order divides that of `g`, then there is a homomorphism `G →+ G'` mapping `g` to `g'`. -/
]
noncomputable def monoidHomOfForallMemZpowers : G →* G'
where
toFun x := g' ^ (Classical.choose <| mem_zpowers_iff.mp <| hg x)
map_one' :=
orderOf_dvd_iff_zpow_eq_one.mp <|
(Int.natCast_dvd_natCast.mpr hg').trans <|
orderOf_dvd_iff_zpow_eq_one.mpr <| Classical.choose_spec <| mem_zpowers_iff.mp <| hg 1
map_mul' x
y := by
simp only [← zpow_add, zpow_eq_zpow_iff_modEq]
apply Int.ModEq.of_dvd (Int.natCast_dvd_natCast.mpr hg')
rw [← zpow_eq_zpow_iff_modEq, zpow_add]
simp only [fun x ↦ Classical.choose_spec <| mem_zpowers_iff.mp <| hg x]
