Theorems · Definition · ring theory

DirectSum.GdistribMulAction.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 : GradedMonoid.GMonoid A} →
                {inst_3 : (i : ιB) → AddMonoid (M i)} →
                  {t : DirectSum.GdistribMulAction 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 : GradedMonoid.GMonoid A'} →
                                  {inst'_3 : (i : ιB') → AddMonoid (M' i)} →
                                    {t' : DirectSum.GdistribMulAction A' M'} →
                                      ιA = ιA' →
                                        ιB = ιB' →
                                          A ≍ A' →
                                            M ≍ M' →
                                              inst ≍ inst' →
                                                inst_1 ≍ inst'_1 →
                                                  inst_2 ≍ inst'_2 →
                                                    inst_3 ≍ inst'_3 →
                                                      t ≍ t' → DirectSum.GdistribMulAction.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