OAI/Geometry/IsometricImmersion/Immersions/RankOne2.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothLocal.Geometry.two_by_two_rank_pos line 12
2. theorem OAI.SmoothLocal.Geometry.two_by_two_rank_eq_one_of_ne_zero_det_eq_zero line 27
3. theorem OAI.SmoothLocal.Geometry.two_by_two_rank_eq_one_iff line 44