Theorems · Theorem · group theory

mul_smul_comm

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

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

Defined in

Mathlib.Algebra.Group.Action.Defs

Cited by

65 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

MulSMulSMulCommClass