ofNat_mul_im — Mathlib

English

For any n ≥ 2 and z ∈ K, the imaginary part of the product of ofNat(n) with z equals the product of ofNat(n) and the imaginary part of z.

Русский

Для любого n ≥ 2 и z ∈ K, мнимая часть произведения ofNat(n) на z равна произведению ofNat(n) и мнимой части z.

LaTeX

$$$$\forall n \in \mathbb{N},\ n \ge 2,\ \operatorname{Im}(\operatorname{ofNat}(n) \cdot z) = \operatorname{ofNat}(n) \cdot \operatorname{Im}(z). $$$$

Lean4

theorem ofNat_mul_im (n : ℕ) [n.AtLeastTwo] (z : K) : im (ofNat(n) * z) = ofNat(n) * im z := by
  rw [← ofReal_ofNat, im_ofReal_mul]

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