OAI/Combinatorics/PolynomialVacuum/Cylinder/IceCurrent.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PolynomialVacuumCylinder.dartSign_ne_zero line 9
  2. theorem OAI.PolynomialVacuumCylinder.orientedFlow_eq_zero_iff line 12
  3. theorem OAI.PolynomialVacuumCylinder.flow_zero_outside_vertices line 17
  4. theorem OAI.PolynomialVacuumCylinder.outgoingSlot_ne line 27
  5. theorem OAI.PolynomialVacuumCylinder.wordContour_localIce line 30
  6. theorem OAI.PolynomialVacuumCylinder.simple_word_localIce line 39
  7. theorem OAI.PolynomialVacuumCylinder.LocalIce.sum_zero line 50
  8. theorem OAI.PolynomialVacuumCylinder.allLocalIce_conserved line 58
  9. theorem OAI.PolynomialVacuumCylinder.Conserved.sum_zero line 68
  10. theorem OAI.PolynomialVacuumCylinder.ClosedNetwork.component_flow_localIce line 80
  11. theorem OAI.PolynomialVacuumCylinder.ClosedNetwork.component_oriented_at line 86