mathlib documentation

algebra.star.algebra

Star algebras

Introduces the notion of a star algebra over a star ring.

@[class]
structure star_algebra (R : Type u) (A : Type v) [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] :
Type

A star algebra A over a star ring R is an algebra which is a star ring, and the two star structures are compatible in the sense star (r • a) = star r • star a.

@[simp]
theorem star_smul (R : Type u) (A : Type v) [comm_semiring R] [star_ring R] [semiring A] [star_ring A] [algebra R A] [star_algebra R A] (r : R) (a : A) :
star (r a) = star r star a