Theorems · Theorem · group theory
QuotientGroup.lift_surjective_of_surjective
∀ {G : Type u_1} {M : Type u_4} [inst : Group G] [inst_1 : Monoid M] (N : Subgroup G) [nN : N.Normal] (φ : G →* M),
Function.Surjective ⇑φ → ∀ (HN : N ≤ φ.ker), Function.Surjective ⇑(QuotientGroup.lift N φ HN)- Defined in
- Mathlib.GroupTheory.QuotientGroup.Defs
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- GroupMonoidSubgroup.Normal
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Groupstatement and proof · cited by 6,238
- Monoidstatement and proof · cited by 3,887
- MonoidHomstatement and proof · cited by 3,629
- Subgroupstatement and proof · cited by 3,593
- HasQuotient.Quotientstatement · cited by 2,301
- Subgroup.Normalstatement and proof · cited by 334
- MonoidHom.kerstatement and proof · cited by 212
- QuotientGroup.liftstatement · cited by 8
- QuotientGroup.conproof · cited by 7
- Quotient.lift_surjectiveproof · cited by 4
Cited by1
Results whose statement or proof uses this declaration.
- QuotientGroup.map_surjective_of_surjectiveproof · cited by 1