lean_workbook_plus_34130

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that $u+u=2u$ in a vector space $(V,K,+,\cdot)$ , where $u \in V$ and $K$ is a field of scalars.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_34130 (V : Type*) (K : Type*) [Field K] [AddCommGroup V] [Module K V] (u : V) : u + u = 2 • u   :=  by sorry

Source