mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

feat (Algebra/FreeMonoid) : define set of symbols in free monoid element

Open hannahfechtner opened this issue 1 year ago • 1 comments

We add a separate file in which the set of symbols of a FreeMonoid element is defined. This is separated so that users of the basic FreeMonoid file need not unnecessarily import the finiteness hierarchy (as symbols is defined as a Finset)


Open in Gitpod

hannahfechtner avatar Oct 22 '24 01:10 hannahfechtner