Theorems · Inductive type · group theory

AddGroupExtension.Splitting

{N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : AddGroup N] → [inst_1 : AddGroup E] → [inst_2 : AddGroup G] → AddGroupExtension N E G → Type (max u_2 u_3)

Splitting of an additive group extension is a section homomorphism.

Defined in

Mathlib.GroupTheory.GroupExtension.Defs

Cited by

11 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

AddGroupAddGroupAddGroup