feat(combinatorics/simple_graph): Locally linear graphs

leanprover-community / mathlib

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

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

Apache License 2.0

1.66k stars 297 forks source link

Closed YaelDillies closed 7 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 8 months ago

This PR/issue depends on:

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

YaelDillies commented 7 months ago

Ported to LeanCamCombi.