ofReal_comp_nsmul — Mathlib

English

The embedding commutes with natural-scalar multiplication: ofReal ∘ (n • f) = n • (ofReal ∘ f).

Русский

Встраивание сохраняет умножение на натуральное число: ofReal ∘ (n • f) = n • (ofReal ∘ f).

LaTeX

$$$\\operatorname{ofReal} \\circ (n \\cdot f) = n \\cdot (\\operatorname{ofReal} \\circ f)$$$

Lean4

theorem ofReal_comp_nsmul (n : ℕ) (f : α → ℝ) : ofReal ∘ (n • f) = n • (ofReal ∘ f) :=
  map_comp_nsmul ofRealHom ..

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