Theorems · Theorem · group theory

smul_assoc

∀ {α : Type u_5} {M : Type u_9} {N : Type u_10} [inst : SMul M N] [inst_1 : SMul N α] [inst_2 : SMul M α]
  [IsScalarTower M N α] (x : M) (y : N) (z : α), (x • y) • z = x • y • z

Defined in

Mathlib.Algebra.Group.Action.Defs

Cited by

150 results in Mathlib

Foundations

Depth 5 from the axioms, rests on 8 definitions · uses no axioms

Assumes

SMulSMulSMulIsScalarTower