English
The image of a quotient is torsion if and only if the whole group is torsion, given the kernel is torsion.
Русский
Образ факторгруппы торсионен тогда и только тогда, когда вся группа торсионна при условии, что ядро торсионно.
LaTeX
$$$IsTorsion(H) \Leftrightarrow IsTorsion(G)$, при сюръективном $f:G\to H$ и $\ker f$ торсионно.$$
Lean4
/-- The image of a quotient is torsion iff the group is torsion. -/
@[to_additive AddIsTorsion.quotient_iff /-- The image of a quotient is additively torsion iff the group is torsion. -/
]
theorem quotient_iff {f : G →* H} (hf : Function.Surjective f) (hN : N = f.ker) (tN : IsTorsion N) :
IsTorsion H ↔ IsTorsion G :=
⟨fun tH => IsTorsion.extension_closed hN tH tN, fun tG => IsTorsion.of_surjective hf tG⟩
