ofCauchy_mul

Mathlib.Data.Real.Basic

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

English

The embedding preserves multiplication: ofCauchy(a b) = ofCauchy(a) · ofCauchy(b).

Русский

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

LaTeX

$$$$\operatorname{ofCauchy}(a b) = \operatorname{ofCauchy}(a) \cdot \operatorname{ofCauchy}(b).$$$$

Lean4

theorem ofCauchy_mul (a b) : (⟨a * b⟩ : ℝ) = ⟨a⟩ * ⟨b⟩ :=
  (mul_def _ _).symm

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

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

Разделы

Аффилиация

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