Theorems · Theorem · group theory

IsSimpleAddGroup.isSimpleAddGroup_of_surjective

∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_3} [inst_1 : AddGroup H] [IsSimpleAddGroup G] [Nontrivial H]
  (f : G →+ H), Function.Surjective ⇑f → IsSimpleAddGroup H

Defined in

Mathlib.GroupTheory.Subgroup.Simple

Cited by

1 results in Mathlib

Foundations

Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddGroupAddGroupIsSimpleAddGroupNontrivial