smul — Mathlib

English

If r is self-adjoint and x is self-adjoint in a Star-module, then r does not destroy self-adjointness: r • x is self-adjoint.

Русский

Пусть r самосопряжённый, а x — самосопряжённый элемент в модуле с действием; тогда скалярное умножение r • x сохраняет самосопряжённость.

LaTeX

$$$IsSelfAdjoint(r) \to IsSelfAdjoint(x) \to IsSelfAdjoint(r \cdot x)$$$

Lean4

@[aesop safe apply]
theorem smul [Star R] [Star A] [SMul R A] [StarModule R A] {r : R} (hr : IsSelfAdjoint r) {x : A}
    (hx : IsSelfAdjoint x) : IsSelfAdjoint (r • x) := by
  simp only [isSelfAdjoint_iff, star_smul, hr.star_eq, hx.star_eq]

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