Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-02 00:17 decb556e

View on Github →

feat(geometry/euclidean/basic): lemmas about angles and distances (#7140)

Estimated changes

Modified src/geometry/euclidean/basic.lean

added theorem euclidean_geometry.angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi

added theorem euclidean_geometry.angle_left_midpoint_eq_pi_div_two_of_dist_eq

added theorem euclidean_geometry.angle_midpoint_eq_pi

added theorem euclidean_geometry.angle_right_midpoint_eq_pi_div_two_of_dist_eq

added theorem euclidean_geometry.dist_eq_abs_sub_dist_iff_angle_eq_zero

added theorem euclidean_geometry.dist_eq_abs_sub_dist_of_angle_eq_zero

added theorem euclidean_geometry.dist_eq_add_dist_iff_angle_eq_pi

added theorem euclidean_geometry.dist_eq_add_dist_of_angle_eq_pi

added theorem euclidean_geometry.dist_left_midpoint_eq_dist_right_midpoint

added theorem euclidean_geometry.left_dist_ne_zero_of_angle_eq_pi

added theorem euclidean_geometry.right_dist_ne_zero_of_angle_eq_pi

added theorem inner_product_geometry.inner_eq_mul_norm_iff_angle_eq_zero

added theorem inner_product_geometry.inner_eq_mul_norm_of_angle_eq_zero

added theorem inner_product_geometry.inner_eq_neg_mul_norm_iff_angle_eq_pi

added theorem inner_product_geometry.inner_eq_neg_mul_norm_of_angle_eq_pi

added theorem inner_product_geometry.norm_add_eq_add_norm_iff_angle_eq_zero

added theorem inner_product_geometry.norm_add_eq_add_norm_of_angle_eq_zero

added theorem inner_product_geometry.norm_add_eq_norm_sub_iff_angle_eq_pi_div_two

added theorem inner_product_geometry.norm_sub_eq_abs_sub_norm_iff_angle_eq_zero

added theorem inner_product_geometry.norm_sub_eq_abs_sub_norm_of_angle_eq_zero

added theorem inner_product_geometry.norm_sub_eq_add_norm_iff_angle_eq_pi

added theorem inner_product_geometry.norm_sub_eq_add_norm_of_angle_eq_pi