ofReal_comp_zsmul — Mathlib

English

The embedding commutes with integer-scalar multiplication: ofReal ∘ (n • f) = n • (ofReal ∘ f) for n ∈ ℤ.

Русский

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

LaTeX

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

Lean4

theorem ofReal_comp_zsmul (n : ℤ) (f : α → ℝ) : ofReal ∘ (n • f) = n • (ofReal ∘ f) :=
  map_comp_zsmul ofRealHom ..

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