Commit 2023-11-30 02:18 d9c853b9

View on Github →

feat: number of edges in a complete graph (#8631)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

added theorem SimpleGraph.card_edgeFinset_le_card_choose_two

added theorem SimpleGraph.card_edgeFinset_top_eq_card_choose_two

added theorem SimpleGraph.edgeFinset_top

added theorem SimpleGraph.edgeSet_subset_setOf_not_isDiag

added theorem SimpleGraph.edgeSet_top

Modified Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean

Modified Mathlib/Data/Sym/Sym2.lean

added theorem Sym2.fromRel_ne