English
There is a real-linear map that sends skew-adjoint elements to self-adjoint elements by multiplying by -i.
Русский
Существует линейное черезReal отображение, которое переводит SkewAdjoint в SelfAdjoint умножением на -i.
LaTeX
$$$\\text{negISMul} : \\operatorname{skewAdjoint} A \\to \\operatorname{selfAdjoint} A, \\quad a \\mapsto -i \\cdot a$$$
Lean4
/-- Create a `selfAdjoint` element from a `skewAdjoint` element by multiplying by the scalar
`-Complex.I`. -/
@[simps]
def negISMul : skewAdjoint A →ₗ[ℝ] selfAdjoint A
where
toFun
a :=
⟨-I • ↑a, by
simp only [neg_smul, neg_mem_iff, selfAdjoint.mem_iff, star_smul, star_def, conj_I, star_val_eq, smul_neg,
neg_neg]⟩
map_add' a
b := by
ext
simp only [AddSubgroup.coe_add, smul_add, AddMemClass.mk_add_mk]
map_smul' a
b := by
ext
simp only [neg_smul, skewAdjoint.val_smul, RingHom.id_apply, selfAdjoint.val_smul, smul_neg, neg_inj]
rw [smul_comm]
