OAI/Analysis/OperatorAlgebra/FiniteOperatorExtension.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite-dimensional Hilbert-operator form of the matrix cpc extension theorem. An orthonormal basis transports the matrix extension without changing its positivity or norm.

  1. theorem OAI.WeakPureInfiniteness.finiteOperator_cpc_extension line 19