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.

Estimated changes