Theorems · Theorem · linear algebra
Matrix.submatrix_id_id
∀ {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α), A.submatrix id id = A- Defined in
- Mathlib.LinearAlgebra.Matrix.Defs
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Matrixstatement and proof · cited by 4,303
- Matrix.extproof · cited by 540
- Matrix.submatrixstatement · cited by 183
Cited by22
Results whose statement or proof uses this declaration.
- LinearMap.charpoly_toMatrixproof · cited by 9
- Matrix.mul_eq_one_comm_of_equivproof · cited by 4
- Matrix.lift_cRank_submatrixproof · cited by 3
- Matrix.det_comm'proof · cited by 3
- Matrix.fromBlocks_submatrix_sum_swap_sum_swapproof · cited by 2
- Matrix.mem_subfield_of_mul_eq_one_of_mem_subfield_rightproof · cited by 1
- Matrix.isHermitian_submatrix_equivproof · cited by 1
- Matrix.submatrix_mul_transpose_submatrixproof · cited by 1
- Matrix.isAdjMatrix_submatrix_iffproof · cited by 1
- Matrix.posSemidef_submatrix_equivproof · cited by 1
- Matrix.isDetpBalanced_submatrix_equiv_iffproof · cited by 1