15 Linear and multilinear algebra; matrix theory

TheoremBinomial inverse theorem#

The Binomial Inverse Theorem (⅟ version).

See Matrix.invOf_add_mul_mul for the Woodbury identity.

Matrix.invOf_add_mul_mul'.{u_1, u_2, u_3} {m : Type u_1} {n : Type u_2} {α : Type u_3} [Fintype n]
  [DecidableEq n] [Fintype m] [DecidableEq m] [Ring α] (A : Matrix n n α) (U : Matrix n m α)
  (C : Matrix m m α) (V : Matrix m n α) [Invertible A] [Invertible (C + C * V * ⅟A * U * C)]
  [Invertible (A + U * C * V)] :
  ⅟(A + U * C * V) = ⅟A - ⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A
Sources
MathlibMatrix.invOf_add_mul_mul'
Uses 5
Statement usesFinite set · Integer · Invertible elements · Ring · Ring-valued matrix

TheoremBirkhoff–Von Neumann theorem#

Birkhoff's theorem The set of doubly stochastic matrices is the convex hull of the permutation matrices. Note exists_eq_sum_perm_of_mem_doublyStochastic gives a convex weighting of each permutation matrix directly. To show doublyStochastic n is convex, use convex_doublyStochastic.

doublyStochastic_eq_convexHull_permMatrix.{u_1, u_2} {R : Type u_1} {n : Type u_2} [Fintype n]
  [DecidableEq n] [Field R] [LinearOrder R] [IsStrictOrderedRing R] :
  ↑(doublyStochastic R n) = (convexHull R) {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}
Sources
MathlibdoublyStochastic_eq_convexHull_permMatrix
Uses 8
Statement usesConvex hull of a subset of an affine real space · Field · Finite set · Ordered ring · Rational number · Ring-valued matrix
Proof usesCharacteristic zero · Hall's marriage theorem

TheoremDimension theorem for vector spaces#

The dimension theorem: if v and v' are two bases, their index types have the same cardinalities.

mk_eq_mk_of_basis.{u, v, w, w'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M]
  [_root_.Module R M] {ι : Type w} {ι' : Type w'} [InvariantBasisNumber R] (v : Module.Basis ι R M)
  (v' : Module.Basis ι' R M) :
  Cardinal.lift.{w', w} (Cardinal.mk ι) = Cardinal.lift.{w, w'} (Cardinal.mk ι')
Sources
Mathlibmk_eq_mk_of_basis
Uses 5
Statement usesBasis · Cardinal
Proof usesCharacteristic zero · Generating sets · Linear independence

TheoremGershgorin circle theorem#

Gershgorin's circle theorem: for any eigenvalue μ of a square matrix A, there exists an index k such that μ lies in the closed ball of center the diagonal term A k k and of radius the sum of the norms ∑ j ≠ k, ‖A k j‖.

eigenvalue_mem_ball.{u_1, u_2} {K : Type u_1} {n : Type u_2} [NormedField K] [Fintype n]
  [DecidableEq n] {A : Matrix n n K} {μ : K} (hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ) :
  ∃ k, μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.univ.erase k, ‖A k j‖)
Sources
Mathlibeigenvalue_mem_ball
Uses 9
Statement usesAssociative algebra over a commutative ring · Eigenvalue · Finite set · Metric space · Ring-valued matrix
Proof usesEigenvector · Field \(\R\) of real numbers · Ordered ring · The Triangle Inequality

TheoremRank–nullity theorem#

The rank-nullity theorem

LinearMap.rank_range_add_rank_ker.{u, u_1} {R : Type u_1} {M M₁ : Type u} [Ring R] [AddCommGroup M]
  [AddCommGroup M₁] [_root_.Module R M] [_root_.Module R M₁] [HasRankNullity.{u, u_1} R]
  (f : M →ₗ[R] M₁) : Module.rank R ↥f.range + Module.rank R ↥f.ker = Module.rank R M
Sources
MathlibLinearMap.rank_range_add_rank_ker
Uses 5
Statement usesCardinal · Kernel of a linear map · Linear independence · Quotient space (Fundamentals) · Range of a linear map

TheoremSylvester's determinant theorem#

The Weinstein–Aronszajn identity. Note the 1 on the LHS is of shape m×m, while the 1 on the RHS is of shape n×n.

Matrix.det_one_add_mul_comm.{u_2, u_3, u_4} {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m]
  [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m n α) (B : Matrix n m α) :
  (1 + A * B).det = (1 + B * A).det
Sources
MathlibMatrix.det_one_add_mul_comm
Uses 2
Statement usesDeterminant
Proof usesInvertible elements

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.