Theorems · Inductive type · ring theory

GradedMonoid.GSMul

{ιA : Type u_1} →
  {ιM : Type u_3} → (ιA → Type u_4) → (ιM → Type u_5) → [VAdd ιA ιM] → Type (max (max (max u_1 u_3) u_4) u_5)

A graded version of SMul. Scalar multiplication combines grades additively, i.e. if a ∈ A i and m ∈ M j, then a • b must be in M (i + j).

Defined in

Mathlib.Algebra.GradedMulAction

Cited by

1 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

VAdd