English
For an additive group G and an element g ∈ G, the kernel of the homomorphism zmultiplesHom G g is exactly the subgroup generated by addOrderOf g.
Русский
Для аддитивной группы G и элемента g ∈ G ядро гомоморфизма zmultiplesHom G g совпадает с подгруппой, порождаемой addOrderOf g.
LaTeX
$$$\ker\bigl(\mathrm{zmultiplesHom}(G,g)\bigr) = \mathrm{zmultiples}\bigl(\operatorname{addOrderOf}(g)\bigr)$$$
Lean4
/-- The kernel of `zmultiplesHom G g` is equal to the additive subgroup generated by
`addOrderOf g`. -/
theorem zmultiplesHom_ker_eq [AddGroup G] (g : G) : (zmultiplesHom G g).ker = zmultiples ↑(addOrderOf g) :=
by
ext
simp_rw [AddMonoidHom.mem_ker, mem_zmultiples_iff, zmultiplesHom_apply, ← addOrderOf_dvd_iff_zsmul_eq_zero,
zsmul_eq_mul', Int.cast_id, dvd_def, eq_comm]
