Theorems · Theorem · group theory

MonoidHom.liftOfRightInverseAux_comp_apply

∀ {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [inst : Group G₁] [inst_1 : Group G₂] [inst_2 : Group G₃]
  (f : G₁ →* G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : G₁ →* G₃) (hg : f.ker ≤ g.ker) (x : G₁),
  (f.liftOfRightInverseAux f_inv hf g hg) (f x) = g x

Defined in

Mathlib.Algebra.Group.Subgroup.Basic

Cited by

1 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext, Quot.sound

Assumes

GroupGroupGroup