Theorems · Theorem · ring theory

DirectSum.GdistribMulAction.smul_add

∀ {ι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)} [self : DirectSum.GdistribMulAction A M]
  {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

Defined in

Mathlib.Algebra.Module.GradedModule

Cited by

0 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

DirectSum.GdistribMulAction