decompose_eq_mul_idempotent — Mathlib

English

The i-th component of decompose x equals x multiplied by the idempotent e_i, where e_i = idempotent V i.

Русский

i-й компонент разложения x равен умножению x на idempotent e_i, где e_i = idempotent V i.

LaTeX

$$$\operatorname{decompose}_V(x)_i = x \cdot \operatorname{idempotent}(V,i)$$$

Lean4

theorem decompose_eq_mul_idempotent (x : R) (i : I) : decompose V x i = x * idempotent V i := by
  rw [← smul_eq_mul (a := x), idempotent, ← Submodule.coe_smul, ← smul_apply, ← decompose_smul, smul_eq_mul, mul_one]

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