Theorems · Definition · linear algebra
Matrix.rank
{m : Type um} → {n : Type un} → {R : Type uR} → [Fintype n] → [CommSemiring R] → Matrix m n R → ℕThe rank of a matrix is the rank of its image.
- Defined in
- Mathlib.LinearAlgebra.Matrix.Rank
- Cited by
- 48 results in Mathlib
- Foundations
- Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- FintypeCommSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommSemiringstatement and proof · cited by 10,911
- Fintypestatement and proof · cited by 7,736
- Matrixstatement and proof · cited by 4,303
- Module.finrankproof · cited by 1,770
- LinearMap.rangeproof · cited by 893
- Matrix.mulVecLinproof · cited by 38
Cited by48
Results whose statement or proof uses this declaration.
- Matrix.rank_mul_le_leftstatement and proof · cited by 5
- Matrix.rank_subsingletonstatement · cited by 5
- Matrix.rank_transposestatement and proof · cited by 3
- Matrix.rank_diagonalstatement · cited by 3
- Matrix.rank_eq_finrank_span_colsstatement · cited by 3
- Matrix.rank_le_card_widthstatement · cited by 3
- Matrix.rank_mul_eq_left_of_isUnit_detstatement · cited by 2
- Matrix.rank_mul_eq_right_of_det_mem_nonZeroDivisorsstatement and proof · cited by 2
- Matrix.rank_mul_eq_right_of_det_ne_zerostatement · cited by 2
- Matrix.rank_mul_eq_right_of_isUnit_detstatement · cited by 2
- Matrix.rank_mul_le_rightstatement and proof · cited by 2
- Matrix.rank_conjTranspose_mul_selfstatement · cited by 2