Theorems · Theorem · linear algebra
Matrix.rank_transpose
∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : Field R] [inst_2 : Fintype m]
(A : Matrix m n R), A.transpose.rank = A.rank- Defined in
- Mathlib.LinearAlgebra.Matrix.Rank
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites22
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- RingHom.idproof · cited by 18,349
- LinearMapproof · cited by 10,215
- Fintypestatement and proof · cited by 7,736
- Fieldstatement and proof · cited by 7,404
- Matrixstatement and proof · cited by 4,303
- LinearEquivproof · cited by 3,317
- Module.finrankproof · cited by 1,770
- LinearMap.rangeproof · cited by 893
- Module.Dualproof · cited by 583
- Matrix.transposestatement and proof · cited by 389
- Pi.basisFunproof · cited by 78
Cited by3
Results whose statement or proof uses this declaration.
- Matrix.rank_eq_finrank_span_rowproof · cited by 1
- Configuration.ofField.crossProduct_eq_zero_of_dotProduct_eq_zeroproof · cited by 1
- Matrix.rank_self_mul_transposeproof · cited by 0