selfAdjointPart_comp_subtype_selfAdjoint

English

The self-adjoint part map composed with the inclusion of the self-adjoint submodule is the identity on self-adjoint elements.

Русский

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

LaTeX

$$$(\text{selfAdjointPart})(\text{selfAdjoint.submodule } R A) .\text{subtype} = \mathrm{id}_{\mathrm{selfAdjoint} A}$$$

Lean4

@[simp]
theorem selfAdjointPart_comp_subtype_selfAdjoint : (selfAdjointPart R).comp (selfAdjoint.submodule R A).subtype = .id :=
  LinearMap.ext fun x ↦ x.2.selfAdjointPart_apply R

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