OAI/Analysis/JiangSu/MatrixAlgebras/ContinuousMatrixTraceIdeal.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContinuousMatrixTraceIdeal.PathMatrix line 14
2. def OAI.ContinuousMatrixTraceIdeal.single line 16
3. lemma OAI.ContinuousMatrixTraceIdeal.single_mul line 25
4. lemma OAI.ContinuousMatrixTraceIdeal.single_mul_zero line 30
5. lemma OAI.ContinuousMatrixTraceIdeal.single_vanishes line 36
6. lemma OAI.ContinuousMatrixTraceIdeal.diagonal_equal line 47
7. lemma OAI.ContinuousMatrixTraceIdeal.offdiagonal_zero line 58
8. def OAI.ContinuousMatrixTraceIdeal.entry line 68
9. def OAI.ContinuousMatrixTraceIdeal.tracePath line 71
10. lemma OAI.ContinuousMatrixTraceIdeal.decompose line 74
11. lemma OAI.ContinuousMatrixTraceIdeal.eval_as_single_trace line 81
12. def OAI.ContinuousMatrixTraceIdeal.scalarPath line 107
13. lemma OAI.ContinuousMatrixTraceIdeal.tracePath_scalar line 110
14. theorem OAI.ContinuousMatrixTraceIdeal.scalarization line 117