isSelfAdjoint — Mathlib

English

A strictly positive element is self-adjoint in a star-ordered setting.

Русский

Элемент, строго положительный, является самосопряженным в условиях звездообразной упорядоченности.

LaTeX

$$$ \\mathrm{IsStrictlyPositive}(a) \\rightarrow \\mathrm{IsSelfAdjoint}(a) $$$

Lean4

@[grind →]
theorem isSelfAdjoint [Semiring A] [PartialOrder A] [StarRing A] [StarOrderedRing A] {a : A}
    (ha : IsStrictlyPositive a) : IsSelfAdjoint a :=
  ha.nonneg.isSelfAdjoint

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