Theorems · Definition · ring theory

DirectSum.GdistribMulAction.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 : GradedMonoid.GMonoid A] →
                [inst_3 : (i : ιB) → AddMonoid (M i)] →
                  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)] → DirectSum.GdistribMulAction 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

AddMonoidVAddGradedMonoid.GMonoidAddMonoidAddMonoidVAddGradedMonoid.GMonoidAddMonoid