Theorem Matrix.rank_self_mul_transpose
Modification history
2025-04-09 10:22
Mathlib/Data/Matrix/Rank.lean
chore: use mixin ordered algebraic typeclasses (part 2) (#20595)
Modified Matrix.rank_self_mul_transposeView on Github →2024-08-04 10:58
Mathlib/Data/Matrix/Rank.lean
chore: Address todo in `Data/Matrix/Rank.lean` (#15191) …
Modified Matrix.rank_self_mul_transposeView on Github →