linear_combination_nonneg — Mathlib

English

A is generated by its nonnegative elements: the complex-span of {a ∈ A | 0 ≤ a} equals the whole algebra.

Русский

Алгебра A порождена своими неотрицательными элементами: линейный спан по комплексному полю от {a ∈ A | 0 ≤ a} даёт всю алгебру.

LaTeX

$$Submodule.span Complex {a ∈ A | 0 ≤ a} = ⊤$$

Lean4

theorem linear_combination_nonneg (x : A) : ((ℜ x : A)⁺ - (ℜ x : A)⁻) + (I • (ℑ x : A)⁺ - I • (ℑ x : A)⁻) = x := by
  rw [CFC.posPart_sub_negPart _ (ℜ x).2, ← smul_sub, CFC.posPart_sub_negPart _ (ℑ x).2,
    realPart_add_I_smul_imaginaryPart x]

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