Theorems · Definition · linear algebra
Matrix.toBlock
{m : Type u_2} →
{n : Type u_3} → {α : Type u_12} → Matrix m n α → (p : m → Prop) → (q : n → Prop) → Matrix { a // p a } { a // q a } αLet p pick out certain rows and q pick out certain columns of a matrix M. Then
toBlock M p q is the corresponding block matrix.
- Defined in
- Mathlib.Data.Matrix.Block
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
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.submatrixproof · cited by 183
Cited by15
Results whose statement or proof uses this declaration.
- Matrix.toSquareBlockPropproof · cited by 5
- Matrix.toBlock_mul_eq_addstatement · cited by 2
- Matrix.BlockTriangular.invertibleToBlockstatement and proof · cited by 2
- Matrix.twoBlockTriangular_detproof · cited by 1
- Matrix.toBlock_diagonal_disjointstatement · cited by 1
- Matrix.det_toBlockstatement and proof · cited by 1
- Matrix.toBlock_inverse_eq_zerostatement and proof · cited by 1
- Matrix.toBlock_diagonal_selfstatement and proof · cited by 1
- Matrix.toBlock_one_disjointstatement · cited by 1
- Matrix.toBlock_one_selfstatement · cited by 1
- Matrix.BlockTriangular.inv_toBlockstatement · cited by 1
- Matrix.BlockTriangular.toBlock_inverse_mul_toBlock_eq_onestatement and proof · cited by 1