Theorems · Theorem · group theory

SemiconjBy.smul_right

∀ {M : Type u_1} {α : Type u_5} [inst : SMul M α] [inst_1 : Mul α] [SMulCommClass M α α] [IsScalarTower M α α]
  {x a b : α}, SemiconjBy x a b → ∀ (r : M), SemiconjBy x (r • a) (r • b)

Defined in

Mathlib.Algebra.Group.Action.Defs

Cited by

3 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

SMulMulSMulCommClassIsScalarTower