OAI/Analysis/JiangSu/Nonunital/Hereditary.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NonunitalGamma.sandwichSubalgebra line 16
  2. def OAI.NonunitalGamma.hereditarySubalgebra line 32
  3. def OAI.NonunitalGamma.hereditaryCarrier line 35
  4. lemma OAI.NonunitalGamma.hereditarySubalgebra_coe line 37
  5. instance OAI.NonunitalGamma.hereditarySubalgebra_closed line 40
  6. lemma OAI.NonunitalGamma.hereditary_sqrt_mem line 43
  7. lemma OAI.NonunitalGamma.self_mem_hereditary line 49
  8. lemma OAI.NonunitalGamma.hereditary_sandwich_mem line 58
  9. lemma OAI.NonunitalGamma.sqrt_sandwich_mem_hereditary line 71
  10. lemma OAI.NonunitalGamma.hereditary_complex_smul_mem line 80
  11. lemma OAI.NonunitalGamma.hereditary_realPart_mem line 90
  12. lemma OAI.NonunitalGamma.hereditary_imaginaryPart_mem line 96
  13. lemma OAI.NonunitalGamma.trace_selfAdjoint_im_zero line 103
  14. lemma OAI.NonunitalGamma.trace_zero_selfadjoint_split line 112
  15. theorem OAI.NonunitalGamma.exists_orthogonal_pair_hereditary line 139