toReal_nsmul

Mathlib.Data.ENNReal.Real

URI: https://scilib.ai/kg/mathlib#ENNReal.toReal_nsmul

English

Natural scalar multiplication commutes with toReal: (n • a).toReal = n • a.toReal.

Русский

Натуральное умножение на скаляр и toReal commuting: (n • a).toReal = n • a.toReal.

LaTeX

$$$(n \cdot a).\mathrm{toReal} = n \cdot a.\mathrm{toReal}$$$

Lean4

theorem toReal_nsmul (a : ℝ≥0∞) (n : ℕ) : (n • a).toReal = n • a.toReal := by simp

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

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

Разделы

Аффилиация

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