tsub_div

Mathlib.Algebra.Order.Field.Canonical

URI: https://scilib.ai/kg/mathlib#tsub_div

English

For a suitable ordered ring, division distributes over subtraction: (a − b)/c = a/c − b/c.

Русский

Для подходящего упорядоченного кольца деление распределяется по вычитанию: (a − b)/c = a/c − b/c.

LaTeX

$$$\\frac{a-b}{c}=\\frac{a}{c}-\\frac{b}{c}$$$

Lean4

theorem tsub_div (a b c : α) : (a - b) / c = a / c - b / c := by simp_rw [div_eq_mul_inv, tsub_mul]

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

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

Разделы

Аффилиация

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