Commit 2025-01-26 18:41 fdcb7c69
View on Github →feat: state PEquiv.equiv_toPEquiv_toMatrix
in terms of submatrix
(#21089)
This matches the prose more closely, and also means lemmas about submatrix
can be used.
feat: state PEquiv.equiv_toPEquiv_toMatrix
in terms of submatrix
(#21089)
This matches the prose more closely, and also means lemmas about submatrix
can be used.