mathlib3 documentation

algebra.star.free

A *-algebra structure on the free algebra. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.free_monoid and algebra.free_algebra, to avoid importing algebra.star.basic into the entire hierarchy.

@[simp]
theorem free_monoid.star_of {α : Type u_1} (x : α) :
@[simp]
theorem free_monoid.star_one {α : Type u_1} :

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

@[protected, instance]
def free_algebra.star_ring {R : Type u_1} [comm_semiring R] {X : Type u_2} :

The star ring formed by reversing the elements of products

Equations
@[simp]
theorem free_algebra.star_ι {R : Type u_1} [comm_semiring R] {X : Type u_2} (x : X) :
@[simp]
theorem free_algebra.star_algebra_map {R : Type u_1} [comm_semiring R] {X : Type u_2} (r : R) :