Documentation Verification Report

DegreeSum

📁 Source: Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean

Statistics

Metric	Count
Definitions	0
Theorems `edge_fiber`, `dart_card_eq_sum_degrees`, `dart_card_eq_twice_card_edges`, `dart_edge_fiber_card`, `dart_fst_fiber`, `dart_fst_fiber_card_eq_degree`, `even_card_odd_degree_vertices`, `exists_ne_odd_degree_of_exists_odd_degree`, `odd_card_odd_degree_vertices_ne`, `sum_degrees_eq_twice_card_edges`, `sum_degrees_support_eq_twice_card_edges`, `two_mul_card_edgeFinset`	12
Total	12

SimpleGraph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dart_card_eq_sum_degrees` 📖	mathematical	—	`Fintype.card` `Dart` `Dart.fintype` `Finset.sum` `Nat.instAddCommMonoid` `Finset.univ` `degree` `neighborSetFintype`	—	`Finset.sum_congr` `Finset.card_eq_sum_card_fiberwise` `Finset.coe_univ`
`dart_card_eq_twice_card_edges` 📖	mathematical	—	`Fintype.card` `Dart` `Dart.fintype` `Finset.card` `Sym2` `edgeFinset` `fintypeEdgeSet` `Sym2.instFintype`	—	`Finset.card_univ` `Finset.card_eq_sum_card_fiberwise` `Finset.mem_coe` `mem_edgeFinset` `Dart.edge_mem` `mul_comm` `Finset.sum_const_nat` `dart_edge_fiber_card`
`dart_edge_fiber_card` 📖	mathematical	`Sym2` `Set` `Set.instMembership` `edgeSet`	`Finset.card` `Dart` `Finset.filter` `Dart.edge` `Sym2.instDecidableEq` `Finset.univ` `Dart.fintype`	—	`Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable` `Finset.card_insert_of_notMem` `Finset.mem_singleton` `Dart.symm_ne` `Finset.card_singleton` `Dart.edge_fiber`
`dart_fst_fiber` 📖	mathematical	—	`Finset.filter` `Dart` `Dart.toProd` `Finset.univ` `Dart.fintype` `Finset.image` `Set.Elem` `neighborSet` `instDecidableEqDart` `dartOfNeighborSet` `neighborSetFintype`	—	`Finset.ext` `Dart.adj` `Dart.ext`
`dart_fst_fiber_card_eq_degree` 📖	mathematical	—	`Finset.card` `Dart` `Finset.filter` `Dart.toProd` `Finset.univ` `Dart.fintype` `degree` `neighborSetFintype`	—	`dart_fst_fiber` `card_neighborSet_eq_degree` `Finset.card_image_of_injective` `dartOfNeighborSet_injective`
`even_card_odd_degree_vertices` 📖	mathematical	—	`Even` `Finset.card` `Finset.filter` `Odd` `Nat.instSemiring` `degree` `neighborSetFintype` `Nat.instDecidablePredOdd` `Finset.univ`	—	`sum_degrees_eq_twice_card_edges` `ZMod.natCast_eq_zero_iff_even` `Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable` `ZMod.natCast_ne_zero_iff_odd` `Finset.sum_const` `nsmul_eq_mul` `mul_one` `Finset.sum_congr` `Finset.mem_filter_univ` `ZMod.natCast_eq_one_iff_odd` `Nat.not_even_iff_odd` `Finset.sum_filter_ne_zero` `Nat.cast_sum` `Nat.cast_mul` `ZMod.natCast_self` `MulZeroClass.zero_mul`
`exists_ne_odd_degree_of_exists_odd_degree` 📖	—	`Odd` `Nat.instSemiring` `degree` `neighborSetFintype`	—	—	`odd_card_odd_degree_vertices_ne` `Finset.card_pos` `Finset.mem_filter_univ`
`odd_card_odd_degree_vertices_ne` 📖	mathematical	`Odd` `Nat.instSemiring` `degree` `neighborSetFintype`	`Finset.card` `Finset.filter` `Nat.instDecidablePredOdd` `Finset.univ`	—	`even_card_odd_degree_vertices` `Finset.mem_filter_univ` `Nat.instAtLeastTwoHAddOfNat` `mul_pos_iff_of_pos_left` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `zero_lt_two` `Nat.instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `two_mul` `Finset.card_pos` `Finset.filter.congr_simp` `Finset.filter_filter` `Finset.filter_ne'` `Finset.card_erase_of_mem` `tsub_eq_of_eq_add` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le`
`sum_degrees_eq_twice_card_edges` 📖	mathematical	—	`Finset.sum` `Nat.instAddCommMonoid` `Finset.univ` `degree` `neighborSetFintype` `Finset.card` `Sym2` `edgeFinset` `fintypeEdgeSet` `Sym2.instFintype`	—	`dart_card_eq_sum_degrees` `dart_card_eq_twice_card_edges`
`sum_degrees_support_eq_twice_card_edges` 📖	mathematical	—	`Finset.sum` `Nat.instAddCommMonoid` `Set.toFinset` `support` `Subtype.fintype` `Set` `Set.instMembership` `instDecidablePredMemSetSupport` `degree` `neighborSetFintype` `Finset.card` `Sym2` `edgeFinset` `fintypeEdgeSet` `Sym2.instFintype`	—	`Finset.sum_add_sum_compl` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Finset.sum_eq_zero` `degree_eq_zero_iff_notMem_support` `Set.mem_toFinset` `Finset.mem_compl`
`two_mul_card_edgeFinset` 📖	mathematical	—	`Finset.card` `Sym2` `edgeFinset` `fintypeEdgeSet` `Sym2.instFintype` `Finset.filter` `Adj` `Finset.univ` `instFintypeProd`	—	`dart_card_eq_twice_card_edges` `Finset.card_univ` `Finset.card_bij'` `Finset.mem_filter`

SimpleGraph.Dart

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`edge_fiber` 📖	mathematical	—	`Finset.filter` `SimpleGraph.Dart` `Sym2` `edge` `Sym2.instDecidableEq` `Finset.univ` `fintype` `Finset` `Finset.instInsert` `SimpleGraph.instDecidableEqDart` `Finset.instSingleton` `symm`	—	`Finset.ext` `SimpleGraph.dart_edge_eq_iff`

---

← Back to Index