Star monoids and star rings #
We introduce the basic algebraic notions of star monoids, and star rings.
Star algebras are introduced in
For now we simply do not introduce notations,
as different users are expected to feel strongly about the relative merits of
rᘁ, and so on.
- to_has_involutive_star : has_involutive_star R
- star_mul : ∀ (r s : R), has_star.star (r * s) = (has_star.star s) * has_star.star r
- to_star_monoid : star_monoid R
- star_add : ∀ (r s : R), has_star.star (r + s) = has_star.star r + has_star.star s
*-ring is a ring which is both an ordered ring and a
0 ≤ star r * r for every
(In a Banach algebra, the natural ordering is given by the positive cone
which is the closure of the sums of elements
star r * r.
This ordering makes the Banach algebra an ordered