coe_smul

Mathlib.MeasureTheory.VectorMeasure.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.VectorMeasure.coe_smul

English

The coercion respects scalar multiplication: (r · v) measured on i equals r · v(i).

Русский

Сопоставление сохраняет скалярное умножение: (r · v)(i) = r · v(i).

LaTeX

$$⇑(r • v) = r • ⇑v$$

Lean4

@[simp]
theorem coe_smul (r : R) (v : VectorMeasure α M) : ⇑(r • v) = r • ⇑v :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru