Theorems · Theorem · ring theory

GradedMonoid.mk_smul_mk

∀ {ιA : Type u_1} {ιM : Type u_3} (A : ιA → Type u_4) (M : ιM → Type u_5) [inst : VAdd ιA ιM]
  [inst_1 : GradedMonoid.GSMul A M] {i : ιA} {j : ιM} (a : A i) (b : M j),
  GradedMonoid.mk i a • GradedMonoid.mk j b = GradedMonoid.mk (i +ᵥ j) (GradedMonoid.GSMul.smul a b)

Defined in

Mathlib.Algebra.GradedMulAction

Cited by

0 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

VAddGradedMonoid.GSMul