Theorems · Definition · ring theory

DirectSum.GdistribMulAction.casesOn

{ι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)] →
                {motive : DirectSum.GdistribMulAction A M → Sort u} →
                  (t : DirectSum.GdistribMulAction A M) →
                    ([toGMulAction : GradedMonoid.GMulAction A M] →
                        (smul_add :
                            ∀ {i : ιA} {j : ιB} (a : A i) (b c : M j),
                              GradedMonoid.GSMul.smul a (b + c) =
                                GradedMonoid.GSMul.smul a b + GradedMonoid.GSMul.smul a c) →
                          (smul_zero : ∀ {i : ιA} {j : ιB} (a : A i), GradedMonoid.GSMul.smul a 0 = 0) →
                            motive { toGMulAction := toGMulAction, smul_add := smul_add, smul_zero := smul_zero }) →
                      motive t

Defined in

Mathlib.Algebra.Module.GradedModule

Cited by

0 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

AddMonoidVAddGradedMonoid.GMonoidAddMonoid