mathlib

db53863f - feat(combinatorics/simple_graph/ends): Definition (only) of the ends of a simple_graph. (#17857)

feat(combinatorics/simple_graph/ends): Definition (only) of the ends of a simple_graph. (#17857) Co-authored-by: Anand Rao <anand.rao.art@gmail.com> Co-authored-by: Rémi Bottinelli <bottine@users.noreply.github.com> Co-authored-by: ART0 <18333981+0Art0@users.noreply.github.com> Co-authored-by: Anand Rao <18333981+0art0@users.noreply.github.com>