instCompletelyPositiveMapClass — Mathlib

English

Non-unital star algebra homomorphisms are completely positive.

Русский

Ненулевые звездные алгебра-гомоморфизмы являются полностью положительными отображениями.

LaTeX

$$instCompletelyPositiveMapClass$$

Lean4

/-- Non-unital star algebra homomorphisms are completely positive. -/
instance instCompletelyPositiveMapClass : CompletelyPositiveMapClass F A₁ A₂ where
  map_cstarMatrix_nonneg' φ k M
    hM := by
    change 0 ≤ (mapₙₐ (φ : A₁ →⋆ₙₐ[ℂ] A₂)) M
    exact map_nonneg _ hM

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