mul_sub_left_distrib

Mathlib.Algebra.Ring.Defs

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

English

For α a NonUnitalNonAssocRing, a,b,c: a · (b − c) = a · b − a · c.

Русский

Для α, имеющего структуру NonUnitalNonAssocRing, верно a · (b − c) = a · b − a · c.

LaTeX

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

Lean4

theorem mul_sub_left_distrib (a b c : α) : a * (b - c) = a * b - a * c := by
  simpa only [sub_eq_add_neg, neg_mul_eq_mul_neg] using mul_add a b (-c)

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

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

Разделы

Аффилиация

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