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 Algebra.FreeMonoid and Algebra.FreeAlgebra, to avoid importing Algebra.Star.Basic into the entire hierarchy.

instance FreeMonoid.instStarMul {α : Type u_1} :
theorem FreeMonoid.star_of {α : Type u_1} (x : α) :
theorem FreeMonoid.star_one {α : Type u_1} :
star 1 = 1

Note that star_one is already a global simp lemma, but this one works with dsimp too

instance FreeAlgebra.instStarRing {R : Type u_1} [CommSemiring R] {X : Type u_2} :

The star ring formed by reversing the elements of products

theorem FreeAlgebra.star_ι {R : Type u_1} [CommSemiring R] {X : Type u_2} (x : X) :
theorem FreeAlgebra.star_algebraMap {R : Type u_1} [CommSemiring R] {X : Type u_2} (r : R) :

star as an AlgEquiv

  • FreeAlgebra.starHom = let __src := starRingEquiv; { toEquiv := __src.toEquiv, map_mul' := , map_add' := , commutes' := }
Instances For