realPart_comp_subtype_selfAdjoint

English

The real part map composed with the selfAdjoint submodule’s subtype equals the identity on that subspace.

Русский

Композиция действительной части с подмножеством самосопряжённых элементов равна тождественному отображению на этом подпространстве.

LaTeX

$$$\\text{realPart} \\circ (\\text{selfAdjoint.submodule } \\mathbb{R} A) .\\text{subtype} = \\mathrm{id}$$$

Lean4

theorem realPart_comp_subtype_selfAdjoint : realPart.comp (selfAdjoint.submodule ℝ A).subtype = LinearMap.id :=
  selfAdjointPart_comp_subtype_selfAdjoint ℝ

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