coe_smul — Mathlib

English

The ℝ-valued scalar action agrees with its NNReal version under the coe map.

Русский

Сопоставление по вещественному коэффициенту согласуется с версией по NNReal через отображение включения.

LaTeX

$$$ (r : \mathbb{R}) \cdot j = r \cdot j \quad\text{for } r \in \mathbb{R}_{\ge 0}$$$

Lean4

@[simp]
theorem coe_smul (r : ℝ≥0) : (r : ℝ) • j = r • j := by
  rw [real_smul_def, if_pos (NNReal.coe_nonneg r), Real.toNNReal_coe]

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