The singleton-word language is regular

{w} is regular for any word w. The Mathlib IsRegular form holds over any alphabet; the Langlib is_RG form (a right-regular grammar) needs a finite terminal alphabet.

theorem singletonWordLanguage_isRegular {T : Type} (w : List T) : (singletonWordLanguage w).IsRegular

The singleton-word language {w} is regular (Mathlib IsRegular).

theorem singletonWordLanguage_is_RG {T : Type} [Fintype T] (w : List T) : is_RG (singletonWordLanguage w)

The singleton-word language {w} is regular (Langlib is_RG).