Theorems · Theorem · group theory

AddGroupExtension.Splitting.mk.inj

∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} {inst : AddGroup N} {inst_1 : AddGroup E} {inst_2 : AddGroup G}
  {S : AddGroupExtension N E G} {toAddMonoidHom : G →+ E}
  {rightInverse_rightHom : Function.RightInverse (↑toAddMonoidHom).toFun ⇑S.rightHom} {toAddMonoidHom_1 : G →+ E}
  {rightInverse_rightHom_1 : Function.RightInverse (↑toAddMonoidHom_1).toFun ⇑S.rightHom},
  { toAddMonoidHom := toAddMonoidHom, rightInverse_rightHom := rightInverse_rightHom } =
      { toAddMonoidHom := toAddMonoidHom_1, rightInverse_rightHom := rightInverse_rightHom_1 } →
    toAddMonoidHom = toAddMonoidHom_1

Defined in

Mathlib.GroupTheory.GroupExtension.Defs

Cited by

1 results in Mathlib

Foundations

Depth 17 from the axioms · uses no axioms