Theorems · Definition · group theory

AddGroupExtension.Equiv.noConfusion

{P : Sort u} →
  {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} →
                      {t : S.Equiv S'} →
                        {N' : Type u_1} →
                          {E'_1 : Type u_2} →
                            {G' : Type u_3} →
                              {inst' : AddGroup N'} →
                                {inst'_1 : AddGroup E'_1} →
                                  {inst'_2 : AddGroup G'} →
                                    {S'_1 : AddGroupExtension N' E'_1 G'} →
                                      {E'' : Type u_4} →
                                        {inst'_3 : AddGroup E''} →
                                          {S'' : AddGroupExtension N' E'' G'} →
                                            {t' : S'_1.Equiv S''} →
                                              N = N' →
                                                E = E'_1 →
                                                  G = G' →
                                                    inst ≍ inst' →
                                                      inst_1 ≍ inst'_1 →
                                                        inst_2 ≍ inst'_2 →
                                                          S ≍ S'_1 →
                                                            E' = E'' →
                                                              inst_3 ≍ inst'_3 →
                                                                S' ≍ S'' →
                                                                  t ≍ t' →
                                                                    AddGroupExtension.Equiv.noConfusionType P t t'

Defined in

Mathlib.GroupTheory.GroupExtension.Defs

Cited by

0 results in Mathlib

Foundations

Depth 21 from the axioms · uses Quot.sound