# mathlibdocumentation

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) [star_ring R] [semiring A] [star_ring A] [ A] :
Type
• star_smul : ∀ (r : R) (a : A), star (r a) =

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) [star_ring R] [semiring A] [star_ring A] [ A] [ A] (r : R) (a : A) :
star (r a) = star r star a