invOf_two_smul_add_invOf_two_smul

English

In a module over a ring where 2 is invertible, the average of x with itself equals x: (1/2)•x + (1/2)•x = x.

Русский

Для модуля над кольцом, где 2 обратимо, среднее между x и x равно x: (1/2)•x + (1/2)•x = x.

LaTeX

$$$ \frac{1}{2} x + \frac{1}{2} x = x $$$

Lean4

@[simp]
theorem invOf_two_smul_add_invOf_two_smul (R) [Semiring R] [AddCommMonoid M] [Module R M] [Invertible (2 : R)] (x : M) :
    (⅟2 : R) • x + (⅟2 : R) • x = x :=
  Convex.combo_self invOf_two_add_invOf_two _

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