Theorem SimpleGraph.Adj.degree_pos_left

Modification history

2026-01-24 00:25
Mathlib/Combinatorics/SimpleGraph/Finite.lean
refactor(SimpleGraph/Finite): turn `edgeFinset` into a `def` (#28821) …
Added SimpleGraph.Adj.degree_pos_leftView on Github →