OAI/Analysis/HyperbolicCones/Coordinates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Paper256.symIndex_card line 12
2. theorem OAI.Paper256.coordinate_card line 14
3. theorem OAI.Paper256.symmetricCoordinates_isHermitian line 16
4. def OAI.Paper256.symmetricCoordinateEquiv line 30
5. theorem OAI.Paper256.symmetric_finrank line 46
6. theorem OAI.Paper256.ambient_finrank line 50