Theorems · Theorem · group theory

IsAddTorsion.extension_closed

∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] {N : AddSubgroup G} [inst_1 : AddGroup H] {f : G →+ H},
  N = f.ker → IsAddTorsion H → IsAddTorsion ↥N → IsAddTorsion G

Torsion additive groups are closed under extensions.

Defined in

Mathlib.GroupTheory.Torsion

Cited by

2 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Quot.sound

Assumes

AddGroupAddGroup