ofReal_nsmul — Mathlib

English

For natural n and real r, the real embedding of n•r equals n times r as a complex number.

Русский

Для натурального n и действительного r приведенная в ℂ величина n•r равна n•(r) в комплексной области.

LaTeX

$$$\forall n \in \mathbb{N}, r \in \mathbb{R}, \uparrow(n \cdot r) = n \cdot (r \text{ in } \mathbb{C})$$$

Lean4

@[norm_cast]
theorem ofReal_nsmul (n : ℕ) (r : ℝ) : ↑(n • r) = n • (r : ℂ) := by simp

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