Commit 2024-10-28 15:52 8781866c
View on Github →feat(Algebra/FreeMonoid): set of symbols appearing in an element of the free monoid (#18036) 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)