feat(combinatorics/simple_graph): Locally linear graphs

leanprover-community / mathlib3

Lean 3's obsolete mathematical components library: please use mathlib4

https://leanprover-community.github.io/lean3

Apache License 2.0

1.67k stars 298 forks source link

Closed YaelDillies closed 11 months ago

YaelDillies commented 1 year ago

Define predicates for a graph to have edge-disjoint triangles and to be locally linear (edge-disjoint triangles and each edge belongs to a triangle).

mathlib-dependent-issues-bot commented 1 year ago

This PR/issue depends on:

~~leanprover-community/mathlib#19203~~ By Dependent Issues (🤖). Happy coding!

YaelDillies commented 11 months ago

Ported to LeanCamCombi.