OAI/Analysis/JiangSu/CentralSequences/UnitalTraceKernelSigma.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DirectComparison.trace_kernel_sigma_ideal line 22
2. instance OAI.NormUltra.QuotientAlgebra.(instance at line 119) line 119
3. instance OAI.NormUltra.QuotientAlgebra.(instance at line 120) line 120
4. instance OAI.NormUltra.QuotientAlgebra.(instance at line 133) line 133
5. instance OAI.NormUltra.QuotientAlgebra.(instance at line 136) line 136
6. instance OAI.NormUltra.QuotientAlgebra.(instance at line 137) line 137
7. instance OAI.NormUltra.QuotientAlgebra.(instance at line 139) line 139
8. lemma OAI.NormUltra.QuotientAlgebra.diagonal_one line 141