Theorems · Definition · group theory

AddGroupExtension.IsAddConj

{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) → S.Splitting → S.Splitting → Prop

A splitting of an extension S is N-conjugate to another iff there exists n : N such that the section homomorphism is a conjugate of the other section homomorphism by S.inl n.

Defined in

Mathlib.GroupTheory.GroupExtension.Defs

Cited by

3 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext

Assumes

AddGroupAddGroupAddGroup