mathlib3

feat(combinatorics.simple_graph.ends): A version of Freudenthal-Hopf

#18681

Open