Theorems · Theorem · group theory

smul_mul_assoc

∀ {α : Type u_5} {β : Type u_6} [inst : Mul β] [inst_1 : SMul α β] [IsScalarTower α β β] (r : α) (x y : β),
  r • x * y = r • (x * y)

Note that the IsScalarTower α β β typeclass argument is usually satisfied by Algebra α β.

Defined in

Mathlib.Algebra.Group.Action.Defs

Cited by

77 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

MulSMulIsScalarTower