arg_coe_angle_eq_iff — Mathlib

English

For x,y ∈ ℂ, (arg x : Real.Angle) = arg y if and only if arg x = arg y.

Русский

Для комплексных чисел x,y выполняется: (arg x : Real.Angle) = arg y тогда и только тогда, когда arg x = arg y.

LaTeX

$$$ (\operatorname{arg} x : \text{Real.Angle}) = \operatorname{arg} y \;\Longleftrightarrow\; \operatorname{arg} x = \operatorname{arg} y. $$$

Lean4

@[simp]
theorem arg_coe_angle_eq_iff {x y : ℂ} : (arg x : Real.Angle) = arg y ↔ arg x = arg y := by
  simp_rw [← Real.Angle.toReal_inj, arg_coe_angle_toReal_eq_arg]

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