Commit 2023-05-26 23:07 20940188

View on Github →

feat: port Geometry.Euclidean.Angle.Unoriented.Affine (#4400)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean

added theorem AffineIsometry.angle_map

added theorem AffineSubspace.angle_coe

added theorem EuclideanGeometry.angle_add_const

added theorem EuclideanGeometry.angle_const_add

added theorem EuclideanGeometry.angle_const_sub

added theorem EuclideanGeometry.angle_const_vadd

added theorem EuclideanGeometry.angle_const_vsub

added theorem EuclideanGeometry.angle_eq_angle_of_angle_eq_pi

added theorem EuclideanGeometry.angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi

added theorem EuclideanGeometry.angle_eq_left

added theorem EuclideanGeometry.angle_eq_of_ne

added theorem EuclideanGeometry.angle_eq_pi_iff_sbtw

added theorem EuclideanGeometry.angle_eq_right

added theorem EuclideanGeometry.angle_eq_zero_iff_eq_and_ne_or_sbtw

added theorem EuclideanGeometry.angle_eq_zero_iff_ne_and_wbtw

added theorem EuclideanGeometry.angle_eq_zero_of_angle_eq_pi_left

added theorem EuclideanGeometry.angle_eq_zero_of_angle_eq_pi_right

added theorem EuclideanGeometry.angle_left_midpoint_eq_pi_div_two_of_dist_eq

added theorem EuclideanGeometry.angle_lt_pi_of_not_collinear

added theorem EuclideanGeometry.angle_midpoint_eq_pi

added theorem EuclideanGeometry.angle_ne_pi_of_not_collinear

added theorem EuclideanGeometry.angle_ne_zero_of_not_collinear

added theorem EuclideanGeometry.angle_neg

added theorem EuclideanGeometry.angle_pos_of_not_collinear

added theorem EuclideanGeometry.angle_right_midpoint_eq_pi_div_two_of_dist_eq

added theorem EuclideanGeometry.angle_sub_const

added theorem EuclideanGeometry.angle_vadd_const

added theorem EuclideanGeometry.angle_vsub_const

added theorem EuclideanGeometry.collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi

added theorem EuclideanGeometry.collinear_iff_eq_or_eq_or_sin_eq_zero

added theorem EuclideanGeometry.collinear_of_angle_eq_pi

added theorem EuclideanGeometry.collinear_of_angle_eq_zero

added theorem EuclideanGeometry.collinear_of_sin_eq_zero

added theorem EuclideanGeometry.continuousAt_angle

added theorem EuclideanGeometry.dist_eq_abs_sub_dist_iff_angle_eq_zero

added theorem EuclideanGeometry.dist_eq_abs_sub_dist_of_angle_eq_zero

added theorem EuclideanGeometry.dist_eq_add_dist_iff_angle_eq_pi

added theorem EuclideanGeometry.dist_eq_add_dist_of_angle_eq_pi

added theorem EuclideanGeometry.left_dist_ne_zero_of_angle_eq_pi

added theorem EuclideanGeometry.right_dist_ne_zero_of_angle_eq_pi

added theorem EuclideanGeometry.sin_ne_zero_of_not_collinear

added theorem EuclideanGeometry.sin_pos_of_not_collinear

added theorem Sbtw.angle₁₂₃_eq_pi

added theorem Sbtw.angle₁₃₂_eq_zero

added theorem Sbtw.angle₂₁₃_eq_zero

added theorem Sbtw.angle₂₃₁_eq_zero

added theorem Sbtw.angle₃₁₂_eq_zero

added theorem Sbtw.angle₃₂₁_eq_pi

added theorem Wbtw.angle₁₃₂_eq_zero_of_ne

added theorem Wbtw.angle₂₁₃_eq_zero_of_ne

added theorem Wbtw.angle₂₃₁_eq_zero_of_ne

added theorem Wbtw.angle₃₁₂_eq_zero_of_ne