English
There is a linear map selfAdjointPart: A → selfAdjoint A sending x to its self-adjoint part, namely (1/2) · (x + x*) which lies in the self-adjoint submodule.
Русский
Существует линейное отображение selfAdjointPart: A → selfAdjoint A, отправляющее элемент x в его самосопряжённую часть, равную (1/2)·(x + x*) и принадлежащую подподмодулю самосопряжённых.
LaTeX
$$$\text{selfAdjointPart}: A \to \mathrm{selfAdjoint} A, \quad \text{selfAdjointPart}(x) = \frac{1}{2}(x + x^{*})$$$
Lean4
/-- The self-adjoint part of an element of a star module, as a linear map. -/
@[simps]
def selfAdjointPart : A →ₗ[R] selfAdjoint A
where
toFun
x := ⟨(⅟2 : R) • (x + star x), by rw [selfAdjoint.mem_iff, star_smul, star_trivial, star_add, star_star, add_comm]⟩
map_add' x
y := by
ext
simp [add_add_add_comm]
map_smul' r
x := by
ext
simp [← mul_smul, show ⅟2 * r = r * ⅟2 from Commute.invOf_left <| (2 : ℕ).cast_commute r]
