FreeMonoid.star_one

theorem FreeMonoid.star_one : ∀ {α : Type u_1}, star 1 = 1

This theorem, `FreeMonoid.star_one`, states that for any type `α`, the `star` function applied to `1` is equal to `1`. This means that the `star` function, when applied to the identity element of the multiplicative monoid (1), does not change its value. The comment also indicates that while there exists a global simplification lemma, `star_one`, this version works with the `dsimp` simplification tactic as well in Lean 4.

More concisely: For any type α, the `star` function applied to the identity element 1 is equal to 1. (In other words, the `star` operation is idempotent with respect to 1 in the monoid of α.)