OAI/Geometry/Borsuk/MatrixGeometry/MatrixNorm.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BorsukNine.matrix_action_norm_sq line 16
2. lemma OAI.BorsukNine.sqrt_action_norm_sq line 25
3. lemma OAI.BorsukNine.matrix_sqrt_smul line 29
4. lemma OAI.BorsukNine.matrix_sqrt_range line 43