neg_smul_neg

Mathlib.Algebra.Module.Defs

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

English

For r ∈ R and x ∈ M, (-r) · (-x) = r · x.

Русский

Для r ∈ R и x ∈ M, (-r) · (-x) = r · x.

LaTeX

$$$\\forall r \\in R\\, \\forall x \\in M:\\ (-r) \\cdot (-x) = r \\cdot x$$$

Lean4

theorem neg_smul_neg : -r • -x = r • x := by rw [neg_smul, smul_neg, neg_neg]

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

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

Разделы

Аффилиация

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