Theorems · Theorem · group theory

QuotientAddGroup.quotientKerEquivOfRightInverse_symm_apply

∀ {G : Type u} [inst : AddGroup G] {H : Type v} [inst_1 : AddGroup H] (φ : G →+ H) (ψ : H → G)
  (hφ : Function.RightInverse ψ ⇑φ) (a : H),
  (QuotientAddGroup.quotientKerEquivOfRightInverse φ ψ hφ).symm a = (QuotientAddGroup.mk ∘ ψ) 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

AddGroupAddGroup