Theorems · Theorem · ring theory

DirectSum.Gmodule.smulAddMonoidHom_apply_of_of

∀ {ι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) → AddCommMonoid (A i)] [inst_3 : (i : ιB) → AddCommMonoid (M i)] [inst_4 : DecidableEq ιA]
  [inst_5 : DecidableEq ιB] [inst_6 : GradedMonoid.GMonoid A] [inst_7 : DirectSum.Gmodule A M] {i : ιA} {j : ιB}
  (x : A i) (y : M j),
  ((DirectSum.Gmodule.smulAddMonoidHom A M) ((DirectSum.of A i) x)) ((DirectSum.of M j) y) =
    (DirectSum.of M (i +ᵥ j)) (GradedMonoid.GSMul.smul x y)

Defined in

Mathlib.Algebra.Module.GradedModule

Cited by

1 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddMonoidVAddAddCommMonoidAddCommMonoidDecidableEqDecidableEqGradedMonoid.GMonoidDirectSum.Gmodule