Theorems · Definition · ring theory

DirectSum.Gmodule.noConfusion

{P : Sort u} →
  {ιA : Type u_1} →
    {ιB : Type u_2} →
      {A : ιA → Type u_3} →
        {M : ιB → Type u_4} →
          {inst : AddMonoid ιA} →
            {inst_1 : VAdd ιA ιB} →
              {inst_2 : (i : ιA) → AddMonoid (A i)} →
                {inst_3 : (i : ιB) → AddMonoid (M i)} →
                  {inst_4 : GradedMonoid.GMonoid A} →
                    {t : DirectSum.Gmodule A M} →
                      {ιA' : Type u_1} →
                        {ιB' : Type u_2} →
                          {A' : ιA' → Type u_3} →
                            {M' : ιB' → Type u_4} →
                              {inst' : AddMonoid ιA'} →
                                {inst'_1 : VAdd ιA' ιB'} →
                                  {inst'_2 : (i : ιA') → AddMonoid (A' i)} →
                                    {inst'_3 : (i : ιB') → AddMonoid (M' i)} →
                                      {inst'_4 : GradedMonoid.GMonoid A'} →
                                        {t' : DirectSum.Gmodule A' M'} →
                                          ιA = ιA' →
                                            ιB = ιB' →
                                              A ≍ A' →
                                                M ≍ M' →
                                                  inst ≍ inst' →
                                                    inst_1 ≍ inst'_1 →
                                                      inst_2 ≍ inst'_2 →
                                                        inst_3 ≍ inst'_3 →
                                                          inst_4 ≍ inst'_4 →
                                                            t ≍ t' → DirectSum.Gmodule.noConfusionType P t t'

Defined in

Mathlib.Algebra.Module.GradedModule

Cited by

0 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms