Commit 2023-01-04 14:42 6d0adfa7
View on Github →feat(geometry/euclidean/angle/sphere): law of sines, converse of inscribed angles (#17992) Add some (oriented angle) versions of the law of sines / sine rule, and of the converse of angles in the same segment / opposite angles of a cyclic quadrilateral. As with previous lemmas in this area, more versions would be appropriate to add in future, including unoriented angle versions and versions of the law of sines that don't involve the circumradius and so can be applied even in the degenerate case of collinear points, but this seems a reasonable starting point.
Estimated changes
added theorem affine.triangle.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_circumcenter
added theorem euclidean_geometry.sphere.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center