neg — Mathlib

English

Under a star-preserving map, the image of a self-adjoint element is self-adjoint.

Русский

Пусть есть отображение, сохраняющее звезду; оно отправляет самосопряжённые элементы в самосопряжённые.

LaTeX

$$$\text{IsSelfAdjoint}(f\,x)$$$

Lean4

@[aesop safe apply]
theorem neg {x : R} (hx : IsSelfAdjoint x) : IsSelfAdjoint (-x) := by
  simp only [isSelfAdjoint_iff, star_neg, hx.star_eq]

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