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

[hannahfechtner]

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)

---

[github-actions[bot]]

PR summary b4fbe4083d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Algebra.FreeMonoid.Symbols	404

---

Declarations diff

+ mem_symbols + symbols + symbols_mul + symbols_of + symbols_one

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style