smul_mem_skewAdjoint — Mathlib

English

For a skew-adjoint element x in R, star(x) equals -x.

Русский

Для кососопряжённого элемента x в R star(x) = -x.

LaTeX

$$$ \\star x = -x \\quad \\text{for } x \\in \\mathrm{skewAdjoint}(R). $$$

Lean4

/-- Scalar multiplication of a self-adjoint element by a skew-adjoint element produces a
skew-adjoint element. -/
theorem smul_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 : IsSelfAdjoint a) : r • a ∈ skewAdjoint A :=
  (star_smul _ _).trans <| (congr_arg₂ _ hr ha).trans <| neg_smul _ _

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