arg_coe_angle_toReal_eq_arg — Mathlib

English

Let z be a complex number. The real-valued angle obtained by viewing arg z as a Real.Angle and applying toReal equals arg z itself; i.e. (arg z : Real.Angle).toReal = arg z.

Русский

Пусть z — комплексное число. Реальный угол, получаемый из arg z посредством приведения к Real.Angle и применения toReal, равен arg z; т.е. (arg z : Real.Angle).toReal = arg z.

LaTeX

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

Lean4

@[simp]
theorem arg_coe_angle_toReal_eq_arg (z : ℂ) : (arg z : Real.Angle).toReal = arg z :=
  by
  rw [Real.Angle.toReal_coe_eq_self_iff_mem_Ioc]
  exact arg_mem_Ioc _

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