mk_mul

Mathlib.Data.Real.Basic

URI: https://scilib.ai/kg/mathlib#Real.mk_mul

English

The embedding preserves multiplication: mk(f * g) = mk(f) * mk(g).

Русский

Встраивание сохраняет умножение: mk(f * g) = mk(f) * mk(g).

LaTeX

$$$$\\operatorname{mk}(f \\cdot g) = \\operatorname{mk}(f) \\cdot \\operatorname{mk}(g)$$$$

Lean4

theorem mk_mul {f g : CauSeq ℚ abs} : mk (f * g) = mk f * mk g := by simp [mk, ← ofCauchy_mul]

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

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

Разделы

Аффилиация

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