OAI/Geometry/Borsuk/MatrixGeometry/BlockLine.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BorsukNine.positiveLine_eigenvector line 17
2. lemma OAI.BorsukNine.blockScalar_positiveLine line 22
3. lemma OAI.BorsukNine.blockOff_positiveLine line 26
4. lemma OAI.BorsukNine.blockCorner_positiveLine line 30
5. lemma OAI.BorsukNine.blockCompress_isUnit line 40
6. lemma OAI.BorsukNine.posDef_inner_pos line 63
7. lemma OAI.BorsukNine.blockCompress_negative line 71