Commit 2022-12-06 17:02 10ac9529

View on Github →

feat(geometry/euclidean/angle/oriented): base angles of isosceles triangles are acute (#17823) Add some versions of the lemma that (oriented) based angles of isosceles triangles are acute.

Estimated changes

Modified src/geometry/euclidean/angle/oriented/affine.lean

added theorem euclidean_geometry.abs_oangle_left_to_real_lt_pi_div_two_of_dist_eq

added theorem euclidean_geometry.abs_oangle_right_to_real_lt_pi_div_two_of_dist_eq

Modified src/geometry/euclidean/angle/oriented/basic.lean

added theorem orientation.abs_oangle_sub_left_to_real_lt_pi_div_two

added theorem orientation.abs_oangle_sub_right_to_real_lt_pi_div_two