imaginaryPart_comp_subtype_selfAdjoint

English

ImaginaryPart composed with the selfAdjoint subtype vanishes: Im ∘ subtype_selfAdjoint = 0.

Русский

Мнимая часть после вложения самосопряжённых элементов равна 0.

LaTeX

$$$\\operatorname{imaginaryPart} \\circ (\\text{subtype} \\text{ selfAdjoint}) = 0$$$

Lean4

theorem imaginaryPart_comp_subtype_selfAdjoint : imaginaryPart.comp (selfAdjoint.submodule ℝ A).subtype = 0 := by
  rw [imaginaryPart, LinearMap.comp_assoc, skewAdjointPart_comp_subtype_selfAdjoint, LinearMap.comp_zero]

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