English
For any group G and element g, the kernel of zpowersHom G g is the subgroup generated by the order of g, viewed multiplicatively.
Русский
Для группы G и элемента g ядро zpowersHom G g равно подгруппе, порождающей порядок элемента g, с точкой зрения мультипликативной записи.
LaTeX
$$$\ker\bigl(\mathrm{zpowersHom}(G,g)\bigr) = \mathrm{zpowers}\bigl(\mathrm{Multiplicative}(\operatorname{ofAdd}(\operatorname{orderOf}(g)))\bigr)$$$
Lean4
/-- The kernel of `zpowersHom G g` is equal to the subgroup generated by `orderOf g`. -/
theorem zpowersHom_ker_eq [Group G] (g : G) : (zpowersHom G g).ker = zpowers (Multiplicative.ofAdd ↑(orderOf g)) :=
congr_arg AddSubgroup.toSubgroup <| zmultiplesHom_ker_eq (Additive.ofMul g)
