arg_coe_angle_eq_iff_eq_toReal — Mathlib

English

Let z be a complex number and θ a Real.Angle. Then (arg z : Real.Angle) = θ if and only if arg z = θ.toReal.

Русский

Пусть z — комплексное число, θ — угол Real.Angle. Тогда (arg z : Real.Angle) = θ тогда и только тогда, когда arg z = θ.toReal.

LaTeX

$$$ (\operatorname{arg} z : \text{Real.Angle}) = \theta \;\Longleftrightarrow\; \operatorname{arg} z = \theta.\mathrm{toReal} $$$

Lean4

theorem arg_coe_angle_eq_iff_eq_toReal {z : ℂ} {θ : Real.Angle} : (arg z : Real.Angle) = θ ↔ arg z = θ.toReal := by
  rw [← Real.Angle.toReal_inj, arg_coe_angle_toReal_eq_arg]

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