isStarNormal — Mathlib

English

If x is self-adjoint, then it is star-normal; equivalently, x commutes with its star.

Русский

Если x самосопряжён, то x звёздно-нормален; то есть xCommutator с x* равен нулю.

LaTeX

$$$\text{IsSelfAdjoint}(x) \rightarrow \text{IsStarNormal}(x)$$$

Lean4

@[aesop 10% apply]
theorem isStarNormal {R : Type*} [Mul R] [Star R] {x : R} (hx : IsSelfAdjoint x) : IsStarNormal x :=
  ⟨by simp only [Commute, SemiconjBy, hx.star_eq]⟩

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