Theorems · Theorem · group theory

smul_mul_smul_comm

∀ {α : Type u_5} {β : Type u_6} [inst : Mul α] [inst_1 : Mul β] [inst_2 : SMul α β] [IsScalarTower α β β]
  [IsScalarTower α α β] [SMulCommClass α β β] (a : α) (b : β) (c : α) (d : β), a • b * c • d = (a * c) • (b * d)

Note that the IsScalarTower α β β and SMulCommClass α β β typeclass arguments are usually satisfied by Algebra α β.

Defined in

Mathlib.Algebra.Group.Action.Defs

Cited by

14 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

MulMulSMulIsScalarTowerIsScalarTowerSMulCommClass