Theorem orientation.rotation_eq_basis_rotation
Modification history
2022-10-24 11:01
src/geometry/euclidean/oriented_angle.lean
feat(geometry/euclidean/oriented_angle): refactor to a basis-free definition (#16596) …
Deleted orientation.rotation_eq_basis_rotationView on Github →