A *-algebra structure on the free algebra. #
Reversing words gives a *-structure on the free monoid or on the free algebra on a type.
Implementation note #
We have this in a separate file, rather than in
to avoid importing
algebra.star.basic into the entire hierarchy.
star_one is already a global simp lemma, but this one works with dsimp too
The star ring formed by reversing the elements of products