coe_mul — Mathlib

English

Coercion commutes with multiplication: the real value of the product equals the product of the real values.

Русский

Коэрцирование сохраняет умножение: действительное значение произведения равно произведению действительных значений.

LaTeX

$$$ ((r_1 * r_2 : \mathbb{R}_{\ge 0}) : \mathbb{R}) = r_1 * r_2 $$$

Lean4

@[simp, norm_cast]
protected theorem coe_mul (r₁ r₂ : ℝ≥0) : ((r₁ * r₂ : ℝ≥0) : ℝ) = r₁ * r₂ :=
  rfl

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