combo_self — Mathlib

English

Let R be a semiring and M a module over R. If a, b ∈ R satisfy a + b = 1, then for all x ∈ M, a · x + b · x = x.

Русский

Пусть R — полугруппа, M — модуль над R. Если a, b ∈ R удовлетворяют a + b = 1, то для каждого x ∈ M выполняется a · x + b · x = x.

LaTeX

$$$\\forall a,b \\in R\\, (a + b = 1) \\Rightarrow \\forall x \\in M\\, a \\cdot x + b \\cdot x = x$$$

Lean4

theorem combo_self {a b : R} (h : a + b = 1) (x : M) : a • x + b • x = x := by rw [← add_smul, h, one_smul]

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