Matrices

TheoremChange of basis#

Mathlib states this as basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix.

basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix.{u_1, u_2, u_3, u_4, u_5, u_6, u_9}
  {ι : Type u_1} {ι' : Type u_2} {κ : Type u_3} {κ' : Type u_4} {R : Type u_5} {M : Type u_6}
  [CommSemiring R] [AddCommMonoid M] [_root_.Module R M] {N : Type u_9} [AddCommMonoid N]
  [_root_.Module R N] (b : Module.Basis ι R M) (b' : Module.Basis ι' R M) (c : Module.Basis κ R N)
  (c' : Module.Basis κ' R N) (f : M →ₗ[R] N) [Fintype ι'] [Finite κ] [Fintype ι] [Fintype κ']
  [DecidableEq ι] [DecidableEq ι'] :
  c.toMatrix ⇑c' * (LinearMap.toMatrix b' c') f * b'.toMatrix ⇑b = (LinearMap.toMatrix b c) f
Sources
Mathlibbasis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix
Uses 1
Statement usesMatrix representation of a linear map

DefinitionRank of a matrix#

The rank of a matrix is the rank of its image.

Matrix.rank.{um, un, uR} {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [CommSemiring R]
  (A : Matrix m n R) : ℕ
Sources
MathlibMatrix.rank
Uses 5
Statement usesAssociative algebra over a commutative ring · Cardinal · Linear independence · Range of a linear map · Ring-valued matrix

TheoremGaussian elimination#

Any matrix can be reduced to diagonal form by elementary operations.

Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal.{u_1, u_3} {n : Type u_1}
  {𝕜 : Type u_3} [Field 𝕜] [DecidableEq n] [Fintype n] (M : Matrix n n 𝕜) :
  ∃ L L' D,
    (List.map Matrix.TransvectionStruct.toMatrix L).prod * M *
        (List.map Matrix.TransvectionStruct.toMatrix L').prod =
      Matrix.diagonal D
Sources
MathlibMatrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal
Uses 5
Statement usesField · Finite set · Rational number · Ring-valued matrix
Proof usesAssociative algebra over a commutative ring

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.