Theorems · Definition · linear algebra

Matrix.col

{m : Type u_2} → {n : Type u_3} → {α : Type v} → Matrix m n α → n → m → α

For an m × n α-matrix A, A.col j is the jth column of A as a vector in m → α. A.col is defeq to Aᵀ, but refers to the 'column function' of A while avoiding defeq abuse and noisy eta-expansions (and without the simplifier unfolding transposes) in expressions like Set.Injective A.col and Set.range A.col. (Note 2025-04-07 : the identifier Matrix.col used to refer to a matrix with all columns equal; this is now called Matrix.replicateCol)

Defined in

Mathlib.LinearAlgebra.Matrix.Defs

Cited by

56 results in Mathlib

Foundations

Depth 15 from the axioms · uses Quot.sound