connectivity): open a namespace block for `connected_component` (#18520)

Commit

2 years ago

chore(combinatorics/simple_graph/connectivity): open a namespace block for `connected_component` (#18520) Co-authored-by: Rémi Bottinelli <bottine@users.noreply.github.com>

Author

bottine

Parents

35882ddc

mathlib e876965f - chore(combinatorics/simple_graph/connectivity): open a namespace block for `connected_component` (#18520)

mathlib
e876965f - chore(combinatorics/simple_graph/connectivity): open a namespace block for `connected_component` (#18520)