Law of Sines for Euclidean Geometry Triangles

Stream: Is there code for X?

[Chu Zheng]

Hi all,
It seems that the Law of Sines is not currently in Triangle.lean.
I'm not sure whether it has been proved elsewhere. There is an oangle-based version here:EuclideanGeometry.Sphere.dist_div_sin_oangle_eq_two_mul_radius

Just wanted to check in and discuss before opening a PR.

theorem law_sin (x y : V) : Real.sin (angle x y) * ‖x‖ = Real.sin (angle y (x - y)) * ‖x - y‖  := by
  cases eq_or_ne x 0 with
  | inl hxl =>
    simp [hxl]
    cases eq_or_ne y 0 with
    | inl hyl => right; exact hyl
    | inr hyr => left;rw [angle_neg_right,angle_self hyr];simp
  | inr hxr =>
    cases eq_or_ne y 0 with
    | inl hyl => simp [hyl]
    | inr hyr =>
      cases eq_or_ne x y with
      | inl hxy =>
        rw [hxy]
        simp;left
        rw [angle_self hyr,Real.sin_zero]
      | inr hxy =>
        have hsub: x - y ≠ 0 :=by exact sub_ne_zero_of_ne hxy
        have h_sin (x y: V) (hx: x ≠ 0) (hy: y ≠ 0):
          Real.sin (angle x y) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖) :=by
          field_simp [sin_angle_mul_norm_mul_norm]
        rw [h_sin x y hxr hyr, h_sin y (x - y) hyr hsub]
        field_simp
        rw [mul_assoc,mul_assoc]
        congr 1
        · congr 1
          simp_rw [inner_sub_left,inner_sub_right]
          rw [real_inner_comm x y]
          ring_nf
        · ring_nf

theorem law_sin' (x y : V) (hx : x ≠ 0) (hxy: x - y ≠ 0) :
  Real.sin (angle x y) / ‖x - y‖ = Real.sin (angle y (x - y)) / ‖x‖ := by
  field_simp; exact law_sin x y

[Chu Zheng]

@Joseph Myers @Eric Wieser

[Joseph Myers]

@Jovan Gerbscheid had !3#18214 which also had a version of the law of sines, but so far no-one has ported the Euclidean parts of that to Lean 4 (plus that PR was incomplete, it has some sorrys).

[Chu Zheng]

Thanks @Joseph Myers ! I’ve looked at !3#18214, and I’d like to port that to Lean 4 based on the previous work in Lean 3.

[Chu Zheng]

Hi @Joseph Myers @Jovan Gerbscheid , I’ve opened two PRs related to triangle congruence !4#25175 and the law of sines !4#25174. It seems the review process can take a while, so I’ve just been waiting.

Meanwhile, I’ve also formalized Menelaus’ theorem and Ceva’s theorem, which I don’t think are in Mathlib yet. I'm wondering whether I should wait for the previous PRs to be merged before opening new ones.

[Chu Zheng]

I’m very interested in contributing more to Euclidean geometry in Mathlib, but as a new member of the community, I’m not sure what the best way to collaborate is. Any suggestions or advice would be greatly appreciated!

[Joseph Myers]

Note that both Menelaus and Ceva (and their converses) are most naturally given as affine statements, not Euclidean (and not involving the notion of distance), certainly for an arbitrary affine space over a field, maybe over a ring if things work in a more general context such as that (don't know if commutativity is needed or not). Ceva at least also can be done in an n-dimensional version with a 2-dimensional version then deduced from that; see various past discussions.

[Joseph Myers]

(The angle version of Ceva is a genuinely Euclidean result, but that's not the main version.)

[Chu Zheng]

Joseph Myers said:

Note that both Menelaus and Ceva (and their converses) are most naturally given as affine statements, not Euclidean (and not involving the notion of distance), certainly for an arbitrary affine space over a field, maybe over a ring if things work in a more general context such as that (don't know if commutativity is needed or not). Ceva at least also can be done in an n-dimensional version with a 2-dimensional version then deduced from that; see various past discussions.

Thank you for the information and guidance!
I’ll take a closer look at how to formalize both Menelaus and Ceva in affine geometry, or more general context, rather than restricting to Euclidean one.