Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-14 08:08 fdc326c0

View on Github →

feat(geometry/euclidean): sum of angles of a triangle (#2994) Item 27 from the 100-theorems list.

Estimated changes

Modified src/geometry/euclidean.lean

added theorem euclidean_geometry.angle_add_angle_add_angle_eq_pi

added theorem inner_product_geometry.angle_add_angle_sub_add_angle_sub_eq_pi

added theorem inner_product_geometry.cos_angle_add_angle_sub_add_angle_sub_eq_neg_one

added theorem inner_product_geometry.cos_angle_sub_add_angle_sub_rev_eq_neg_cos_angle

added theorem inner_product_geometry.sin_angle_add_angle_sub_add_angle_sub_eq_zero

added theorem inner_product_geometry.sin_angle_sub_add_angle_sub_rev_eq_sin_angle