Theorems · Theorem · ring theory

DirectSum.Gmodule.add_smul

∀ {ι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}
  [self : DirectSum.Gmodule A M] {i : ιA} {j : ιB} (a a' : A i) (b : M j),
  GradedMonoid.GSMul.smul (a + a') b = GradedMonoid.GSMul.smul a b + GradedMonoid.GSMul.smul a' b

Defined in

Mathlib.Algebra.Module.GradedModule

Cited by

0 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

DirectSum.Gmodule