OAI/Combinatorics/PolynomialVacuum/Cylinder/SystemCurrent.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolynomialVacuumCylinder.signedPolygonCurrent line 9
2. theorem OAI.PolynomialVacuumCylinder.signedPolygonCurrent_support line 12
3. theorem OAI.PolynomialVacuumCylinder.signedPolygonCurrent_localIce line 16
4. def OAI.PolynomialVacuumCylinder.systemCurrent line 22
5. theorem OAI.PolynomialVacuumCylinder.systemCurrent_at line 25
6. theorem OAI.PolynomialVacuumCylinder.systemCurrent_outside line 36
7. theorem OAI.PolynomialVacuumCylinder.systemCurrent_localIce line 45
8. theorem OAI.PolynomialVacuumCylinder.ice_current_orientation_decomposition line 58