Theorems · Theorem · group theory

QuotientAddGroup.lift_surjective_of_surjective

∀ {G : Type u_1} {M : Type u_4} [inst : AddGroup G] [inst_1 : AddMonoid M] (N : AddSubgroup G) [nN : N.Normal]
  (φ : G →+ M), Function.Surjective ⇑φ → ∀ (HN : N ≤ φ.ker), Function.Surjective ⇑(QuotientAddGroup.lift N φ HN)

Defined in

Mathlib.GroupTheory.QuotientGroup.Defs

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddGroupAddMonoidAddSubgroup.Normal