Commit 2023-06-14 07:38 798cd59e

View on Github →

feat: port Geometry.Euclidean.Triangle (#5036)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Euclidean/Triangle.lean

added theorem EuclideanGeometry.angle_add_angle_add_angle_eq_pi

added theorem EuclideanGeometry.angle_eq_angle_of_dist_eq

added theorem EuclideanGeometry.dist_eq_of_angle_eq_angle_of_angle_ne_pi

added theorem EuclideanGeometry.dist_mul_of_eq_angle_of_dist_mul

added theorem EuclideanGeometry.dist_sq_add_dist_sq_eq_two_mul_dist_midpoint_sq_add_half_dist_sq

added theorem EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle

added theorem EuclideanGeometry.dist_sq_mul_dist_add_dist_sq_mul_dist

added theorem EuclideanGeometry.oangle_add_oangle_add_oangle_eq_pi

added theorem InnerProductGeometry.angle_add_angle_sub_add_angle_sub_eq_pi

added theorem InnerProductGeometry.angle_sub_eq_angle_sub_rev_of_norm_eq

added theorem InnerProductGeometry.cos_angle_add_angle_sub_add_angle_sub_eq_neg_one

added theorem InnerProductGeometry.cos_angle_sub_add_angle_sub_rev_eq_neg_cos_angle

added theorem InnerProductGeometry.norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi

added theorem InnerProductGeometry.norm_sub_sq_eq_norm_sq_add_norm_sq_sub_two_mul_norm_mul_norm_mul_cos_angle

added theorem InnerProductGeometry.sin_angle_add_angle_sub_add_angle_sub_eq_zero

added theorem InnerProductGeometry.sin_angle_sub_add_angle_sub_rev_eq_sin_angle