Commit 2026-07-27 12:15 dfdaed47

View on Github →

feat(GroupTheory/FreeGroup/IsFreeGroup): to_additive'ize file (#42109) Add additive analogs of FreeGroupBasis/IsFreeGroup and apply @[to_additive] throughout the rest of the file.

Estimated changes

added structure FreeAddGroupBasis
modified theorem FreeGroupBasis.map_apply