ofNat_mul_re — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem ofNat_mul_re (n : ℕ) [n.AtLeastTwo] (z : K) : re (ofNat(n) * z) = ofNat(n) * re z := by
  rw [← ofReal_ofNat, re_ofReal_mul]

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