Theorems · Definition · group theory

AddGroupExtension.Equiv.casesOn

{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} →
              {E' : Type u_4} →
                [inst_3 : AddGroup E'] →
                  {S' : AddGroupExtension N E' G} →
                    {motive : S.Equiv S' → Sort u} →
                      (t : S.Equiv S') →
                        ((toAddEquiv : E ≃+ E') →
                            (inl_comm : ⇑toAddEquiv ∘ ⇑S.inl = ⇑S'.inl) →
                              (rightHom_comm : ⇑S'.rightHom ∘ ⇑toAddEquiv = ⇑S.rightHom) →
                                motive
                                  { toAddEquiv := toAddEquiv, inl_comm := inl_comm, rightHom_comm := rightHom_comm }) →
                          motive t

Defined in

Mathlib.GroupTheory.GroupExtension.Defs

Cited by

0 results in Mathlib

Foundations

Depth 19 from the axioms · uses Quot.sound

Assumes

AddGroupAddGroupAddGroupAddGroup