Theorems · Definition · group theory

QuotientGroup.kerLift

{G : Type u} → [inst : Group G] → {H : Type v} → [inst_1 : Group H] → (φ : G →* H) → G ⧸ φ.ker →* H

The induced map from the quotient by the kernel to the codomain.

Defined in

Mathlib.GroupTheory.QuotientGroup.Basic

Cited by

8 results in Mathlib

Foundations

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

Assumes

GroupGroup