instCoeToCompletelyPositiveMap — Mathlib

English

Non-unital star homomorphisms into completely positive maps form a completely positive map class.

Русский

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

LaTeX

$$NonUnitalStarAlgHomClass.instCompletelyPositiveMapClass F A₁ A₂$$

Lean4

/-- Reinterpret an element of a type of completely positive maps as a completely positive linear
map. -/
instance instCoeToCompletelyPositiveMap [CompletelyPositiveMapClass F A₁ A₂] : CoeHead F (A₁ →CP A₂) where
  coe f := toCompletelyPositiveLinearMap f

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