div_ofReal — Mathlib

English

For every z in C and every real x, the quotient z/x equals the complex number whose real part is Re(z)/x and imaginary part is Im(z)/x.

Русский

Для каждого z ∈ ℂ и каждого действительного x верно z/x = (Re(z))/x + i (Im(z))/x.

LaTeX

$$$\\dfrac{z}{x} = \\dfrac{\\operatorname{Re}(z)}{x} + i\\,\\dfrac{\\operatorname{Im}(z)}{x}$$$

Lean4

theorem div_ofReal (z : ℂ) (x : ℝ) : z / x = ⟨z.re / x, z.im / x⟩ := by
  simp_rw [div_eq_inv_mul, ← ofReal_inv, ofReal_mul']

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