OAI/Geometry/Borsuk/MatrixGeometry/SymmetricCoordinates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BorsukNine.UpperTriangle line 13
2. def OAI.BorsukNine.symmetricCoordinates line 15
3. lemma OAI.BorsukNine.symmetricCoordinates_upper line 31
4. lemma OAI.BorsukNine.symmetricCoordinates_selfAdjoint line 37
5. lemma OAI.BorsukNine.symmetricCoordinates_injective line 54
6. lemma OAI.BorsukNine.upperTriangle_four_card line 61