mul_div_right_comm

Mathlib.Data.ENNReal.Inv

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

English

For all a,b,c: a * b / c = a / c * b.

Русский

Для всех a,b,c: a * b / c = a / c * b.

LaTeX

$$a * b / c = a / c * b$$

Lean4

protected theorem mul_div_right_comm : a * b / c = a / c * b := by simp only [div_eq_mul_inv, mul_right_comm]

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

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

Разделы

Аффилиация

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