Matrices

DefinitionRing-valued matrix#

Matrix m n R is the type of matrices with entries in R, whose rows are indexed by m and whose columns are indexed by n.

Matrix.{u, u', v} (m : Type u) (n : Type u') (α : Type v) : Type (max u u' v)
Sources
MathlibMatrix
Used by 13
Used byAdjacency matrix · Matrix representation · Determinant · Matrix representation of a linear map · Binomial inverse theorem · Birkhoff–Von Neumann theorem · Gershgorin circle theorem · Wedderburn–Artin theorem · General linear group (Classical automorphism groups) · Orthogonal group · Unitary group · Gaussian elimination · Rank of a matrix

DefinitionMatrix representation of a linear map#

Given bases of two modules M₁ and M₂ over a commutative ring R, we get a linear equivalence between linear maps M₁ →ₗ M₂ and matrices over R indexed by the bases.

LinearMap.toMatrix.{u_1, u_3, u_4, u_5, u_6} {R : Type u_1} [CommSemiring R] {m : Type u_3}
  {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6}
  [AddCommMonoid M₁] [AddCommMonoid M₂] [_root_.Module R M₁] [_root_.Module R M₂]
  (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) : (M₁ →ₗ[R] M₂) ≃ₗ[R] Matrix m n R
Sources
MathlibLinearMap.toMatrix
Uses 3 · Used by 3
Statement usesAssociative algebra over a commutative ring · Isomorphism with \(K^n\) · Ring-valued matrix
Used byChange of coordinates · Change of basis · Determinant of endomorphisms

DefinitionDeterminant#

The determinant of a matrix given by the Leibniz formula.

This is available in bundled forms as: * Matrix.detMonoidHom * Matrix.detRowAlternating

Matrix.det.{v, u_2} {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R]
  (M : Matrix n n R) : R
Sources
MathlibMatrix.det
Uses 6 · Used by 13
Statement usesAlternating map · Associative algebra over a commutative ring · Integer · Linear map · Ring-valued matrix · Signature
Used byCramer’s Rule · Dirichlet class number formula · Dirichlet unit theorem · Characteristic polynomial · Invertibility · Sylvester's determinant theorem · Triple product · General linear group (Classical automorphism groups) · Special orthogonal group · Special unitary group · Determinant of endomorphisms · Determinant of vectors · Special linear group

InstanceInvertibility#

The inverse of a square matrix, when it is invertible (and zero otherwise).

Matrix.inv.{u', v} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] :
  Inv (Matrix n n α)
Sources
MathlibMatrix.inv
Uses 1 · Used by 1
Statement usesDeterminant
Used byChange of variables formula

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.