OAI/Analysis/JiangSu/Nonunital/IdealDensity.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NonunitalGamma.closedTwoSidedIdeal line 15
  2. theorem OAI.NonunitalGamma.coe_closedTwoSidedIdeal line 36
  3. def OAI.NonunitalGamma.finiteIdealSum line 40
  4. def OAI.NonunitalGamma.finiteSandwichIdeal line 43
  5. lemma OAI.NonunitalGamma.finiteIdealSum_dense line 65
  6. theorem OAI.NonunitalGamma.exists_square_finiteIdealSum line 94
  7. theorem OAI.NonunitalGamma.cfc_mem_real_subalgebra line 119
  8. def OAI.NonunitalGamma.hereditaryMatrix line 126
  9. instance OAI.NonunitalGamma.hereditaryMatrix_closed line 141
  10. lemma OAI.NonunitalGamma.matrix_sqrt_hereditary line 149
  11. lemma OAI.NonunitalGamma.sum_star_matrix_vector line 160
  12. lemma OAI.NonunitalGamma.hereditary_matrix_vector_mulStar line 176
  13. theorem OAI.NonunitalGamma.finite_trace_transfer line 189