Commit 2023-03-01 16:36 c17b9637

View on Github →

feat: port Combinatorics.SimpleGraph.Acyclic (#2559)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

added theorem SimpleGraph.IsAcyclic.path_unique

added def SimpleGraph.IsAcyclic

added structure SimpleGraph.IsTree

added theorem SimpleGraph.isAcyclic_iff_forall_adj_isBridge

added theorem SimpleGraph.isAcyclic_iff_forall_edge_isBridge

added theorem SimpleGraph.isAcyclic_iff_path_unique

added theorem SimpleGraph.isAcyclic_of_path_unique

added theorem SimpleGraph.isTree_iff_existsUnique_path