add_div

Mathlib.Data.ENNReal.Inv

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

English

Division distributes over addition: (a+b)/c = a/c + b/c.

Русский

Деление распространяется над суммой: (a+b)/c = a/c + b/c.

LaTeX

$$$\\dfrac{a+b}{c} = \\dfrac{a}{c} + \\dfrac{b}{c}$$$

Lean4

protected theorem add_div : (a + b) / c = a / c + b / c :=
  right_distrib a b c⁻¹

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

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

Разделы

Аффилиация

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