ofReal_comp_mul — Mathlib

English

The embedding preserves multiplication: ofReal ∘ (f · g) = ofReal ∘ f · ofReal ∘ g.

Русский

Встраивание сохраняет умножение: ofReal ∘ (f · g) = ofReal ∘ f · ofReal ∘ g.

LaTeX

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

Lean4

@[simp]
theorem ofReal_comp_mul (f g : α → ℝ) : ofReal ∘ (f * g) = ofReal ∘ f * ofReal ∘ g :=
  map_comp_mul ofRealHom ..

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