Theorems · Theorem · group theory

MonoidHom.domRestrictHomKerEquiv_symm_coe_apply

∀ {G : Type u} [inst : Group G] (A : Type u_1) [inst_1 : CommGroup A] (H : Subgroup G) [inst_2 : H.Normal]
  (f : G ⧸ H →* A) (g : G), ↑((MonoidHom.domRestrictHomKerEquiv A H).symm f) g = f ↑g

Defined in

Mathlib.GroupTheory.QuotientGroup.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupCommGroupSubgroup.Normal