English
The product of a rational (or general) element with a skew-adjoint element can be self-adjoint under suitable conditions.
Русский
Произведение скалярного элемента и кососопряжённого может быть самосопряжённым при подходящих условиях.
LaTeX
$$$ [\\text{Ring } R] [\\text{AddCommGroup } A] [\\text{Module } R A] [\\text{StarModule } R A] \\Rightarrow \\forall r \\in \\mathrm{skewAdjoint}(R), \\; \\forall a \\in \\mathrm{skewAdjoint}(A), \\; IsSelfAdjoint (r \\cdot a). $$$
Lean4
/-- Scalar multiplication of a skew-adjoint element by a skew-adjoint element produces a
self-adjoint element. -/
theorem isSelfAdjoint_smul_of_mem_skewAdjoint [Ring R] [AddCommGroup A] [Module R A] [StarAddMonoid R] [StarAddMonoid A]
[StarModule R A] {r : R} (hr : r ∈ skewAdjoint R) {a : A} (ha : a ∈ skewAdjoint A) : IsSelfAdjoint (r • a) :=
(star_smul _ _).trans <| (congr_arg₂ _ hr ha).trans <| neg_smul_neg _ _
