OAI/Analysis/JiangSu/MatrixAlgebras/FiniteCorners.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Pureness.corner_isometryline 15 - lemma
OAI.Pureness.corner_nonnegline 18
OAI/Analysis/JiangSu/MatrixAlgebras/FiniteCorners.lean2 declarations, 0 contain sorry, 0 declared as axioms
OAI.Pureness.corner_isometry line 15OAI.Pureness.corner_nonneg line 18