of_surjective — Mathlib

English

The image of a surjective torsion group homomorphism is torsion.

Русский

Образ сюръективного гомоморфизма, чьей областью является торсионная группа, тоже торсионен.

LaTeX

$$$f:G\to H$ surjective\;\text{If } IsTorsion(G)\\,\; IsTorsion(H)$.$$

Lean4

/-- The image of a surjective torsion group homomorphism is torsion. -/
@[to_additive AddIsTorsion.of_surjective /--
    The image of a surjective additive torsion group homomorphism is torsion. -/
    ]
theorem of_surjective {f : G →* H} (hf : Function.Surjective f) (tG : IsTorsion G) : IsTorsion H := fun h =>
  by
  obtain ⟨g, hg⟩ := hf h
  rw [← hg]
  exact f.isOfFinOrder (tG g)

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