mathlib

9df8c90d - homotopic maps induce equal maps on homology