Theorems · Theorem · linear algebra
Matrix.rank_reindex
∀ {m : Type um} {m₀ : Type um₀} {n : Type un} {n₀ : Type un₀} {R : Type uR} [inst : Fintype n] [inst_1 : Fintype n₀]
[inst_2 : CommSemiring R] (em : m ≃ m₀) (en : n ≃ n₀) (A : Matrix m n R), ((Matrix.reindex em en) A).rank = A.rank- Defined in
- Mathlib.LinearAlgebra.Matrix.Rank
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- FintypeFintypeCommSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites23
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- RingHom.idproof · cited by 18,349
- CommSemiringstatement and proof · cited by 10,911
- LinearMapproof · cited by 10,215
- Equivstatement and proof · cited by 8,337
- Fintypestatement and proof · cited by 7,736
- Submoduleproof · cited by 7,192
- Matrixstatement and proof · cited by 4,303
- Equiv.symmproof · cited by 3,681
- Module.finrankproof · cited by 1,770
- LinearMap.compproof · cited by 1,642
- LinearEquiv.toLinearMapproof · cited by 1,171
Cited by1
Results whose statement or proof uses this declaration.
- Matrix.rank_submatrixproof · cited by 1