instStarOrderedRing — Mathlib

English

The matrix algebra M_n(𝕜) with the conjugate transpose as involution forms a star-ordered ring: the star operation preserves the order, and addition/multiplication respect positivity.

Русский

Алгебра матриц M_n(𝕜) с сопряжённым транспонированием как инволюция образует звёздно упорядчённое кольцо: операция звезды сохраняет порядок, а сложение и умножение сохраняют неотрицательность.

LaTeX

$$$\mathrm{StarOrderedRing}(M_n(\mathbb{K})).$$$

Lean4

theorem instStarOrderedRing : StarOrderedRing (Matrix n n 𝕜) :=
  .of_nonneg_iff' add_le_add_left fun A ↦
    ⟨fun hA ↦ by
      classical
      obtain ⟨X, hX, -, rfl⟩ :=
        sub_zero A ▸
          CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts hA.isHermitian
            (QuasispectrumRestricts.nnreal_of_nonneg hA.nonneg)
      exact ⟨X, hX.star_eq.symm ▸ rfl⟩,
      fun ⟨A, hA⟩ => hA ▸ (posSemidef_conjTranspose_mul_self A).nonneg⟩

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