Theorems · Definition · ring theory

DirectSum.Gmodule.noConfusionType

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] →
                    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'] → DirectSum.Gmodule A' M' → Sort u

Defined in

Mathlib.Algebra.Module.GradedModule

Cited by

0 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms

Assumes

AddMonoidVAddAddMonoidAddMonoidGradedMonoid.GMonoidAddMonoidVAddAddMonoidAddMonoidGradedMonoid.GMonoid