OAI/Combinatorics/PolynomialVacuum/Cylinder/StackEquiv.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PolynomialVacuumCylinder.StackCoordinates line 9
2. def OAI.PolynomialVacuumCylinder.coordinatesCurrent line 11
3. abbrev OAI.PolynomialVacuumCylinder.LegalStack line 13
4. abbrev OAI.PolynomialVacuumCylinder.BandFlow line 15
5. def OAI.PolynomialVacuumCylinder.recoverCoordinates line 18
6. theorem OAI.PolynomialVacuumCylinder.coordinatesCurrent_injective line 21
7. instance OAI.PolynomialVacuumCylinder.(instance at line 26) line 26
8. instance OAI.PolynomialVacuumCylinder.(instance at line 34) line 34
9. def OAI.PolynomialVacuumCylinder.stackFlowEquiv line 38