mul_comm_div

Mathlib.Data.ENNReal.Inv

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

English

See the identity: a / b * c = a * (c / b).

Русский

См. тождество: a / b * c = a * (c / b).

LaTeX

$$a / b * c = a * (c / b)$$

Lean4

protected theorem mul_comm_div : a / b * c = a * (c / b) := by simp only [div_eq_mul_inv, mul_left_comm, mul_comm]

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

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

Разделы

Аффилиация

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