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

star_smul : ∀ (r : R) (a : A), star (r • a) = has_star.star r • star 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.

Instances

pi.star_algebra

source

@[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