toReal_mul

Mathlib.Data.ENNReal.Real

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

English

The toReal map preserves multiplication: (a · b).toReal = a.toReal · b.toReal.

Русский

toReal сохраняет умножение: (a · b).toReal = a.toReal · b.toReal.

LaTeX

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

Lean4

@[simp]
theorem toReal_mul : (a * b).toReal = a.toReal * b.toReal :=
  toRealHom.map_mul a b

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

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

Разделы

Аффилиация

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