two_smul

Mathlib.Algebra.Module.Defs

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

English

For any module M over R and x ∈ M, (2 : R) · x = x + x.

Русский

Для любого модуля M над R и элемента x ∈ M верно (2 : R) · x = x + x.

LaTeX

$$$\\forall x \\in M\\, (2 : R) \\cdot x = x + x$$$

Lean4

theorem two_smul : (2 : R) • x = x + x := by rw [← one_add_one_eq_two, add_smul, one_smul]

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

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

Разделы

Аффилиация

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