Commit 2020-06-08 19:36 a377993a
View on Github →feat(geometry/euclidean): angles and some basic lemmas (#2865) Define angles (undirected, between 0 and π, in terms of inner product), and prove some basic lemmas involving angles, for real inner product spaces and Euclidean affine spaces. From the 100-theorems list, this provides versions of
- 04 Pythagorean Theorem,
- 65 Isosceles Triangle Theorem and
- 94 The Law of Cosines, with various existing definitions implicitly providing
- 91 The Triangle Inequality.
Estimated changes
added theorem euclidean_geometry.dist_square_eq_dist_square_add_dist_square_sub_two_mul_dist_mul_dist_mul_cos_angle
added theorem inner_product_geometry.norm_add_square_eq_norm_square_add_norm_square_iff_angle_eq_pi_div_two
added theorem inner_product_geometry.norm_sub_square_eq_norm_square_add_norm_square_iff_angle_eq_pi_div_two