OAI/Analysis/Kaplansky/Regular/HilbertTensorModel.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KaplanskyConsequences.Regular.elementary line 15
  2. lemma OAI.KaplanskyConsequences.Regular.elementary_apply line 19
  3. lemma OAI.KaplanskyConsequences.Regular.elementary_inner line 22
  4. def OAI.KaplanskyConsequences.Regular.elementaryBilinear line 28
  5. def OAI.KaplanskyConsequences.Regular.tensorToSum line 36
  6. lemma OAI.KaplanskyConsequences.Regular.tensorToSum_tmul line 38
  7. lemma OAI.KaplanskyConsequences.Regular.tensorToSum_inner line 41
  8. def OAI.KaplanskyConsequences.Regular.tensorToSumIsometry line 50
  9. lemma OAI.KaplanskyConsequences.Regular.elementary_delta line 59
  10. lemma OAI.KaplanskyConsequences.Regular.tensorToSum_dense line 66
  11. abbrev OAI.KaplanskyConsequences.Regular.HilbertTensor line 77
  12. def OAI.KaplanskyConsequences.Regular.tensorCompletionMap line 81
  13. lemma OAI.KaplanskyConsequences.Regular.tensorCompletionMap_coe line 84
  14. def OAI.KaplanskyConsequences.Regular.tensorCompletionIsometry line 89
  15. lemma OAI.KaplanskyConsequences.Regular.tensorCompletionIsometry_surjective line 99
  16. def OAI.KaplanskyConsequences.Regular.tensorHilbertEquiv line 107
  17. lemma OAI.KaplanskyConsequences.Regular.tensorHilbertEquiv_tmul line 110
  18. lemma OAI.KaplanskyConsequences.Regular.diagonal_elementary line 115
  19. lemma OAI.KaplanskyConsequences.Regular.left_elementary line 121