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.

Instances
@[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
@[instance]
def pi.star_algebra {I : Type u} {f : I → Type v} {R : Type w} [comm_semiring R] [Π (i : I), semiring (f i)] [Π (i : I), algebra R (f i)] [star_ring R] [Π (i : I), star_ring (f i)] [Π (i : I), star_algebra R (f i)] :
star_algebra R (Π (i : I), f i)
Equations