OAI/Probability/SpanningForest/IncidenceCirculation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336.IncidenceCirculation.incidence line 14
  2. def OAI.Problem336.IncidenceCirculation.reducedIncidence line 17
  3. theorem OAI.Problem336.IncidenceCirculation.sum_incidence_column line 21
  4. theorem OAI.Problem336.IncidenceCirculation.sum_divergence line 25
  5. theorem OAI.Problem336.IncidenceCirculation.divergence_eq_zero_of_off_root line 32
  6. theorem OAI.Problem336.IncidenceCirculation.reduced_mulVec_eq_zero_iff line 43
  7. theorem OAI.Problem336.IncidenceCirculation.reduced_mulVec_eq_zero_iff_root line 54
  8. def OAI.Problem336.IncidenceCirculation.pushMatrix line 59
  9. theorem OAI.Problem336.IncidenceCirculation.incidence_naturality line 66
  10. theorem OAI.Problem336.IncidenceCirculation.circulation_pushForward line 77
  11. theorem OAI.Problem336.IncidenceCirculation.reduced_circulation_pushForward line 85
  12. theorem OAI.Problem336.IncidenceCirculation.pushMatrix_mulVec_apply line 96
  13. theorem OAI.Problem336.IncidenceCirculation.pushMatrix_mulVec_apply_of_not_mem_range line 103
  14. def OAI.Problem336.IncidenceCirculation.circulationSpace line 110
  15. theorem OAI.Problem336.IncidenceCirculation.reduced_circulationSpace_eq line 113
  16. theorem OAI.Problem336.IncidenceCirculation.circulationSpace_map_le line 120