Theorems · Theorem · group theory

QuotientGroup.quotientKerEquivOfRightInverse_apply

∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (φ : G →* H) (ψ : H → G)
  (hφ : Function.RightInverse ψ ⇑φ) (a : G ⧸ φ.ker),
  (QuotientGroup.quotientKerEquivOfRightInverse φ ψ hφ) a = (QuotientGroup.kerLift φ) a

Defined in

Mathlib.GroupTheory.QuotientGroup.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupGroup