Theorems · Theorem · nonassociative algebras

CentroidHomClass.map_mul_left

∀ {F : Type u_6} {α : outParam (Type u_7)} {inst : NonUnitalNonAssocSemiring α} {inst_1 : FunLike F α α}
  [self : CentroidHomClass F α] (f : F) (a b : α), f (a * b) = a * f b

Commutativity of centroid homomorphisms with left multiplication.

Defined in

Mathlib.Algebra.Ring.CentroidHom

Cited by

3 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CentroidHomClass