Commit 2025-07-15 19:38 54b59e30
View on Github →chore: generalise FreeGroup.ext_hom to monoids (#27140)
Also spell FreeGroup.induction_on using of rather than pure. This lets me move it before ext_hom, so that I can use it in the proof.
From Toric