Theorems · Definition · linear algebra
Matrix.row
{m : Type u_2} → {n : Type u_3} → {α : Type v} → Matrix m n α → m → n → αFor an m × n α-matrix A, A.row i is the ith row of A as a vector in n → α.
A.row is defeq to A, but explicitly refers to the 'row function' of A
while avoiding defeq abuse and noisy eta-expansions,
such as in expressions like Set.Injective A.row and Set.range A.row.
(Note 2025-04-07 : the identifier Matrix.row used to refer to a matrix with all rows equal;
this is now called Matrix.replicateRow)
- Defined in
- Mathlib.LinearAlgebra.Matrix.Defs
- Cited by
- 40 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
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
Cited by40
Results whose statement or proof uses this declaration.
- Matrix.vecMul_injective_iffstatement and proof · cited by 4
- Matrix.single_vecMulstatement · cited by 4
- Matrix.detp_eq_of_row_eqstatement and proof · cited by 3
- Matrix.row_transposestatement · cited by 3
- Matrix.Nonsingular.of_linearIndependent_rowstatement and proof · cited by 2
- Matrix.linearIndependent_row_iffstatement · cited by 2
- Matrix.linearIndependent_rows_iff_isUnitstatement · cited by 2
- Matrix.single_one_vecMulstatement · cited by 2
- Matrix.col_transposestatement · cited by 2
- Matrix.mul_adjp_apply_neproof · cited by 2
- range_vecMulLinearstatement and proof · cited by 2
- Matrix.ext_rowstatement and proof · cited by 2