span_unitary — Mathlib

English

A unital C*-algebra is spanned by its unitary elements over the complex numbers.

Русский

Унитальная C*-алгебра порождается своими единичными элементами над комплексными числами.

LaTeX

$$$\operatorname{span}_{\mathbb{C}}\big(\{u \in A: u \text{ unitary}\}\big) = A$$$

Lean4

/-- A unital C⋆-algebra is spanned by its unitary elements. -/
theorem span_unitary : span ℂ (unitary A : Set A) = ⊤ :=
  by
  rw [eq_top_iff]
  rintro x -
  obtain ⟨u, c, rfl, h⟩ := CStarAlgebra.exists_sum_four_unitary x
  exact sum_mem fun i _ ↦ smul_mem _ _ (subset_span (u i).2)

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