[Merged by Bors] - feat(Geometry/Euclidean/Angle/Oriented): oriented/unoriented equality and bisection lemmas

[jsm28]

Add lemmas

lemma oangle_eq_neg_of_angle_eq_of_sign_eq_neg {w x y z : V}
    (h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z)
    (hs : (o.oangle w x).sign = -(o.oangle y z).sign) : o.oangle w x = -o.oangle y z := by

and

lemma angle_eq_iff_oangle_eq_neg_of_sign_eq_neg {w x y z : V} (hw : w ≠ 0) (hx : x ≠ 0)
    (hy : y ≠ 0) (hz : z ≠ 0) (hs : (o.oangle w x).sign = -(o.oangle y z).sign) :
    InnerProductGeometry.angle w x = InnerProductGeometry.angle y z ↔
      o.oangle w x = -o.oangle y z := by

and similar affine versions, corresponding to such lemmas that already exist when the signs are equal rather than negations of each other. Deduce lemmas relating oriented and unoriented versions of angle bisection:

lemma angle_eq_iff_oangle_eq_or_sameRay {x y z : V} (hx : x ≠ 0) (hz : z ≠ 0) :
    InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔
      o.oangle x y = o.oangle y z ∨ SameRay ℝ x z := by

and

lemma angle_eq_iff_oangle_eq_or_wbtw {p₁ p₂ p₃ p₄ : P} (hp₁ : p₁ ≠ p₂) (hp₄ : p₄ ≠ p₂) :
    ∠ p₁ p₂ p₃ = ∠ p₃ p₂ p₄ ↔ ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ ∨ Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁ := by

---

[github-actions]

PR summary b7404f616c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ angle_eq_iff_oangle_eq_or_sameRay
+ angle_eq_iff_oangle_eq_or_wbtw
++ angle_eq_iff_oangle_eq_neg_of_sign_eq_neg
++ oangle_eq_neg_of_angle_eq_of_sign_eq_neg

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[JovanGerb]

Could you change the order of the lemmas (in both files) so that oangle_eq_neg_of_angle_eq_of_sign_eq_neg and angle_eq_iff_oangle_eq_neg_of_sign_eq_neg come directly after their analogues oangle_eq_of_angle_eq_of_sign_eq and angle_eq_iff_oangle_eq_of_sign_eq?

[jsm28]

Order changed as requested.

[JovanGerb]

Thanks, LGTM 🎉

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by JovanGerb.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Post-Build Step