eq_iff_abs_toReal_eq_of_sign_eq — Mathlib

English

If θ.sign = ψ.sign, then θ = ψ if and only if |θ.toReal| = |ψ.toReal|.

Русский

Если θ.sign = ψ.sign, тогда θ = ψ тогда и только тогда, когда |θ.toReal| = |ψ.toReal|.

LaTeX

$$θ.sign = ψ.sign ⇒ (θ = ψ ⟺ |θ.toReal| = |ψ.toReal|)$$

Lean4

theorem eq_iff_abs_toReal_eq_of_sign_eq {θ ψ : Angle} (h : θ.sign = ψ.sign) : θ = ψ ↔ |θ.toReal| = |ψ.toReal| := by
  simpa [h] using @eq_iff_sign_eq_and_abs_toReal_eq θ ψ

Похожие утверждения