Commit 2023-10-28 19:07 bab05758

feat: change IsFreeGroup to a Prop (#7698) Currently, the class IsFreeGroup contains data (namely, a specific set of generators). This is bad, as there are many sets of generators in a free group, and changing sets of generators happens all the time in geometric group theory. We switch to a design in which

• we define FreeGroupBasis, following the definition and API of bases of vector spaces. Most existing API around IsFreeGroup is transferred to lemmas taking a free group basis as a variable.
• The typeclass IsFreeGroup is Prop-valued, and requires only the existence of a free group basis.