Theorem SimpleGraph.card_neighborSet_eq_degree

Modification history

2024-02-03 03:33

Mathlib/Combinatorics/SimpleGraph/Basic.lean

refactor: split out finiteness properties for simple graphs (#10123)

Modified SimpleGraph.card_neighborSet_eq_degree View on Github →

2023-02-24 18:27

Mathlib/Combinatorics/SimpleGraph/Basic.lean

feat: Port `Combinatorics.SimpleGraph.Basic` (#1883)

Added SimpleGraph.card_neighborSet_eq_degree View on Github →