2022-09-30 21:28
src/geometry/euclidean/oriented_angle.lean
feat(analysis/inner_product/orientation, geometry/euclidean/oriented_angle): use bundled orthonormal bases (#16475) …
Added orthonormal_basis.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq