OAI/Analysis/JiangSu/MatrixAlgebras/FinOneMatrixTransport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Pureness.scalarMatrixHom_finOne_bijective line 15
2. def OAI.Pureness.scalarFinOneEquiv line 32
3. lemma OAI.Pureness.scalarFinOneEquiv_apply line 35
4. lemma OAI.Pureness.scalarFinOneEquiv_symm_apply line 38
5. lemma OAI.Pureness.compress_nonneg line 54
6. lemma OAI.Pureness.matrixRank_compress_le line 60
7. lemma OAI.Pureness.completedCompression_rank_monotone line 68