span_selfAdjoint — Mathlib

English

The complex span of self-adjoint elements equals the whole space: span_C(selfAdjoint A) = ⊤.

Русский

Комплексное замыкание самосопряжённых элементов порождает всё пространство: span_C(selfAdjoint A) = ⊤.

LaTeX

$$$\\operatorname{span}_{\\mathbb{C}}(\\mathrm{selfAdjoint}(A)) = \\top$$$

Lean4

theorem span_selfAdjoint : span ℂ (selfAdjoint A : Set A) = ⊤ :=
  by
  refine eq_top_iff'.mpr fun x ↦ ?_
  rw [← realPart_add_I_smul_imaginaryPart x]
  exact add_mem (subset_span (ℜ x).property) <| SMulMemClass.smul_mem _ <| subset_span (ℑ x).property

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