div_div

Mathlib.Data.EReal.Inv

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

English

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

Русский

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

LaTeX

$$$a / b / c = a / (b \cdot c)$$$

Lean4

theorem div_div (a b c : EReal) : a / b / c = a / (b * c) :=
  by
  change (a * b⁻¹) * c⁻¹ = a * (b * c)⁻¹
  rw [mul_assoc a b⁻¹, mul_inv]

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

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

Разделы

Аффилиация

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