OAI/Analysis/KadisonKastler/MatrixCentralVectorTests.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Matrix-unit tests for central vectors

  1. def OAI.KadisonKastler.rightVectorLinear line 20

    Source documentation

    Right evaluation is linear in the algebra element, despite the two conjugations.

    def rightVectorLinear (J : H ≃ₗᵢ⋆[ℂ] H) (ξ : H) : (H →L[ℂ] H) →ₗ[ℂ] H where
…
  2. theorem OAI.KadisonKastler.rightVectorLinear_apply line 30
  3. theorem OAI.KadisonKastler.mem_centralVectorSpace_matrix_iff line 33