English
There is a linear map skewAdjointPart: A → skewAdjoint A sending x to its skew-adjoint part, namely (1/2) · (x − x*).
Русский
Существует линейное отображение skewAdjointPart: A → skewAdjoint A, отправляющее x в его космодружённую часть, равную (1/2)·(x − x*).
LaTeX
$$$\text{skewAdjointPart}: A \to \mathrm{skewAdjoint} A, \quad \text{skewAdjointPart}(x) = \frac{1}{2}(x - x^{*})$$$
Lean4
/-- The skew-adjoint part of an element of a star module, as a linear map. -/
@[simps]
def skewAdjointPart : A →ₗ[R] skewAdjoint A
where
toFun
x :=
⟨(⅟2 : R) • (x - star x), by
simp only [skewAdjoint.mem_iff, star_smul, star_sub, star_star, star_trivial, ← smul_neg, neg_sub]⟩
map_add' x
y := by
ext
simp only [sub_add, ← smul_add, sub_sub_eq_add_sub, star_add, AddSubgroup.coe_add]
map_smul' r
x := by
ext
simp [← mul_smul, ← smul_sub, show r * ⅟2 = ⅟2 * r from Commute.invOf_right <| (2 : ℕ).commute_cast r]
