Theorems · Definition · ring theory

GradedMonoid.GSMul.smul

{ιA : Type u_1} →
  {ιM : Type u_3} →
    {A : ιA → Type u_4} →
      {M : ιM → Type u_5} →
        {inst : VAdd ιA ιM} → [self : GradedMonoid.GSMul A M] → {i : ιA} → {j : ιM} → A i → M j → M (i +ᵥ j)

The homogeneous multiplication map smul

Defined in

Mathlib.Algebra.GradedMulAction

Cited by

9 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

GradedMonoid.GSMul