Commit 2026-03-04 16:26 4250d1a5

feat(GroupTheory/FreeGroup/Basic): surjection between types induces surjection between free groups on those types (#34624) feat(GroupTheory/FreeGroup/Basic): adds the theorem that if α and β are arbitrary types and there is a surjection between them, then the induced FreeGroup.map is also surjective. This is a dependency of a larger PR to formalize finitely presented groups https://github.com/leanprover-community/mathlib4/pull/34236.