add_smul

Mathlib.RingTheory.PolynomialLaw.Basic

URI: https://scilib.ai/kg/mathlib#PolynomialLaw.add_smul

English

Distributivity of smul over addition: (a+b)•f = a•f + b•f.

Русский

Дистрибутивность смулятора над сложением: (a+b)•f = a•f + b•f.

LaTeX

$$$ (a+b) \cdot f = a \cdot f + b \cdot f $$$

Lean4

theorem add_smul : (a + b) • f = a • f + b • f := by ext; simp only [add_def, smul_def, _root_.add_smul]

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

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

Разделы

Аффилиация

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