mathlib
17219820 - feat(data/matrix/rank): rank of `Aᵀ ⬝ A` and `Aᴴ ⬝ A` (#18818)

Commit
2 years ago
feat(data/matrix/rank): rank of `Aᵀ ⬝ A` and `Aᴴ ⬝ A` (#18818) Since these results imply it trivially, this also includes lemmas about the rank of `Aᵀ` and `Aᴴ`. However, these lemmas are not stated very generally, and are surely true in wider cases than the ones proven here.
Author
Parents
Loading