div_mul_div_comm

Mathlib.Data.EReal.Inv

URI: https://scilib.ai/kg/mathlib#EReal.div_mul_div_comm

← MathLib Explorer

English

Let a, b, c, d be elements of EReal. Then (a / b) · (c / d) = (a · c) / (b · d).

Русский

Пусть a, b, c, d принадлежат EReal. Тогда (a / b) · (c / d) = (a · c) / (b · d).

LaTeX

$$$\dfrac{a}{b} \cdot \dfrac{c}{d} = \dfrac{ac}{bd}$$$

Lean4

theorem div_mul_div_comm (a b c d : EReal) : a / b * (c / d) = a * c / (b * d) := by
  rw [← mul_div a, mul_comm b d, ← div_div c, ← mul_div_left_comm (c / d), mul_comm (a / b)]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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