Matrix

Results named in Tau Ceti's TauCeti.LinearAlgebra.Matrix modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe Bruhat decomposition, counted#

the Borel subgroup of GL₂ over a field has exactly two double cosets, indexed by the Weyl group S₂ of GL₂. This is the input to the Mackey irreducibility criterion for the principal series.

TauCeti.GL2Borel.card_doubleCosetQuotient_eq_two.{u} (F : Type u) [Field F] :
  Nat.card (DoubleCoset.Quotient ↑(TauCeti.GL2Borel F) ↑(TauCeti.GL2Borel F)) = 2
Lean

Formalized in Tau Ceti as TauCeti.GL2Borel.card_doubleCosetQuotient_eq_two.

Other forms

The Bruhat decomposition of GL₂, covering half. Formalized in Tau Ceti as TauCeti.GL2Borel.union_doubleCoset_weyl_eq_univ.

TauCeti.GL2Borel.union_doubleCoset_weyl_eq_univ.{u} (F : Type u) [Field F] :
  ↑(TauCeti.GL2Borel F) ∪
      DoubleCoset.doubleCoset (TauCeti.GL2WeylElement F) ↑(TauCeti.GL2Borel F)
        ↑(TauCeti.GL2Borel F) =
    Set.univ

The Bruhat decomposition of GL₂, disjointness half. Formalized in Tau Ceti as TauCeti.GL2Borel.disjoint_doubleCoset_weyl.

TauCeti.GL2Borel.disjoint_doubleCoset_weyl.{u} (F : Type u) [Field F] :
  Disjoint (↑(TauCeti.GL2Borel F))
    (DoubleCoset.doubleCoset (TauCeti.GL2WeylElement F) ↑(TauCeti.GL2Borel F) ↑(TauCeti.GL2Borel F))
Sources
LeanTauCeti.GL2Borel.card_doubleCosetQuotient_eq_two · TauCeti.GL2Borel.union_doubleCoset_weyl_eq_univ · TauCeti.GL2Borel.disjoint_doubleCoset_weyl

TheoremCauchy--Binet for 2 × 2 minors#

A minor of a product is the sum, over the increasing pairs of the middle index type, of the products of the corresponding minors of the two factors.

Matrix.pairMinor_mul.{u, u_1, u_2, u_3} {m : Type u_1} {n : Type u_2} {R : Type u} [CommRing R]
  {l : Type u_3} [Fintype l] [LinearOrder l] (g : Matrix m l R) (h : Matrix l n R) (p : m × m)
  (q : n × n) : (g * h).pairMinor p q = ∑ ij with ij.1 < ij.2, g.pairMinor p ij * h.pairMinor ij q
Lean

Formalized in Tau Ceti as Matrix.pairMinor_mul.

Other forms

Cauchy--Binet across a four-element middle index type, with the six increasing pairs written out. Formalized in Tau Ceti as Matrix.pairMinor_mul_fin_four.

Matrix.pairMinor_mul_fin_four.{u, u_1, u_2} {m : Type u_1} {n : Type u_2} {R : Type u} [CommRing R]
  (g : Matrix m (Fin 4) R) (h : Matrix (Fin 4) n R) (p : m × m) (q : n × n) :
  (g * h).pairMinor p q =
    g.pairMinor p (0, 1) * h.pairMinor (0, 1) q + g.pairMinor p (0, 2) * h.pairMinor (0, 2) q +
            g.pairMinor p (0, 3) * h.pairMinor (0, 3) q +
          g.pairMinor p (1, 2) * h.pairMinor (1, 2) q +
        g.pairMinor p (1, 3) * h.pairMinor (1, 3) q +
      g.pairMinor p (2, 3) * h.pairMinor (2, 3) q
Sources
LeanMatrix.pairMinor_mul · Matrix.pairMinor_mul_fin_four
Used by 4
Used byThe finite-field generation theorem · The rank-one Bruhat decomposition Sz(q) = B ∪ B w B, for m ≠ 0 · Classification of finite simple groups, statement only · TauCeti.ValidLieTypeIndex.Group

TheoremThe Cauchy--Binet identity for the cross product#

A matrix M sends the cross product of u and w to the cross product of their images up to the transposed adjugate of M: (M u) ⨯₃ (M w) = (adj M)ᵀ (u ⨯₃ w).

Matrix.mulVec_cross_mulVec.{u_1} {R : Type u_1} [CommRing R] (M : Matrix (Fin 3) (Fin 3) R)
  (u w : Fin 3 → R) :
  (crossProduct (M.mulVec u)) (M.mulVec w) = M.adjugate.transpose.mulVec ((crossProduct u) w)
Lean

Formalized in Tau Ceti as Matrix.mulVec_cross_mulVec.

Sources
LeanMatrix.mulVec_cross_mulVec

TheoremCayley–Hamilton in size two#

a 2 × 2 matrix A satisfies A ^ 2 = (trace A) • A - (det A) • 1.

Matrix.sq_eq_trace_smul_sub_det_smul_one_fin_two.{u_1} {R : Type u_1} [CommRing R]
  (A : Matrix (Fin 2) (Fin 2) R) : A ^ 2 = A.trace • A - A.det • 1
Lean

Formalized in Tau Ceti as Matrix.sq_eq_trace_smul_sub_det_smul_one_fin_two.

Other forms

Cayley–Hamilton along a representation. Formalized in Tau Ceti as Matrix.Represents.aeval_charpoly_eq_zero.

Matrix.Represents.aeval_charpoly_eq_zero.{u_1, u_2, u_3} {ι : Type u_1} [Fintype ι] [DecidableEq ι]
  {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [_root_.Module R M] {b : ι → M}
  (hb : Submodule.span R (Set.range b) = ⊤) {A : Matrix ι ι R} {f : Module.End R M}
  (h : Matrix.Represents b A f) : (Polynomial.aeval f) A.charpoly = 0

Cayley–Hamilton in size two, as a recurrence for the powers of a 2 × 2 matrix. Formalized in Tau Ceti as Matrix.pow_add_two_fin_two.

Matrix.pow_add_two_fin_two.{u_1} {R : Type u_1} [CommRing R] (A : Matrix (Fin 2) (Fin 2) R)
  (n : ℕ) : A ^ (n + 2) = A.trace • A ^ (n + 1) - A.det • A ^ n
Sources
LeanMatrix.sq_eq_trace_smul_sub_det_smul_one_fin_two · Matrix.Represents.aeval_charpoly_eq_zero · Matrix.pow_add_two_fin_two
Used by 6
Used byOrbit-torus weights are local zeta factors · Indefinite lattices have infinite isometry groups · Popa–Zagier's ambient trace identity (Popa–Zagier, §2, Propositions 2 and 3) · The Eichler–Selberg trace formula at level one · The universal property of the henselization · The universal property of the henselization of a local ring

TheoremCollatz–Wielandt bound#

Let A be entrywise nonnegative with A v ≤ r v for a vector v all of whose entries are strictly positive. If t y ≤ A y entrywise for some nonzero nonnegative vector y, then t ≤ r.

Matrix.le_of_smul_le_mulVec.{u_1, u_2} {n : Type u_1} [Fintype n] {K : Type u_2} [Semifield K]
  [LinearOrder K] [IsStrictOrderedRing K] {A : Matrix n n K} {v y : n → K} {r t : K}
  (hA : ∀ (i j : n), 0 ≤ A i j) (hv : ∀ (i : n), 0 < v i) (hAv : A.mulVec v ≤ r • v) (hy : 0 ≤ y)
  (hy0 : y ≠ 0) (h : t • y ≤ A.mulVec y) : t ≤ r
Lean

Formalized in Tau Ceti as Matrix.le_of_smul_le_mulVec.

Other forms

Collatz–Wielandt bound for nonnegative matrices. Formalized in Tau Ceti as Matrix.ofReal_le_spectralRadius_of_smul_le_mulVec.

Matrix.ofReal_le_spectralRadius_of_smul_le_mulVec.{u_1} {n : Type u_1} [Fintype n]
  {A : Matrix n n ℝ} (hA : ∀ (i j : n), 0 ≤ A i j) {y : n → ℝ} {t : ℝ} (hy : 0 ≤ y) (hy0 : y ≠ 0)
  (h : t • y ≤ A.mulVec y) : ENNReal.ofReal t ≤ spectralRadius ℂ (A.map Complex.ofReal)
Sources
LeanMatrix.le_of_smul_le_mulVec · Matrix.ofReal_le_spectralRadius_of_smul_le_mulVec
Uses 1 · Used by 1
Proof usesPerron–Frobenius theorem for nonnegative matrices
Used byThe Frobenius–Perron character

TheoremGerstenhaber's theorem#

Over a field with continuous ring operations and closed points in which 0 is not isolated, such as ℂ, a matrix Y lies in the closure of the conjugacy class of a nilpotent matrix X exactly when rank (Y ^ k) ≤ rank (X ^ k) for every k.

Matrix.mem_closure_orbit_iff_forall_rank_pow_le.{u_1, u_2} {n : Type u_1} [Fintype n]
  [DecidableEq n] {K : Type u_2} [Field K] [TopologicalSpace K] [IsTopologicalRing K] [T1Space K]
  [(nhdsWithin 0 {0}ᶜ).NeBot] {X Y : Matrix n n K} (hX : IsNilpotent X) :
  Y ∈ closure (MulAction.orbit (ConjAct (GL n K)) X) ↔ ∀ (k : ℕ), (Y ^ k).rank ≤ (X ^ k).rank
Lean

Formalized in Tau Ceti as Matrix.mem_closure_orbit_iff_forall_rank_pow_le.

Other forms

Gerstenhaber's theorem, Zariski form. Formalized in Tau Ceti as Matrix.mem_zeroLocus_vanishingIdeal_orbit_iff_forall_rank_pow_le.

Matrix.mem_zeroLocus_vanishingIdeal_orbit_iff_forall_rank_pow_le.{u_1, u_2, u_3} {n : Type u_1}
  [Fintype n] [DecidableEq n] {K : Type u_2} [Field K] {k : Type u_3} [Field k] [Algebra k K]
  [Infinite K] {X Y : Matrix n n K} (hX : IsNilpotent X) :
  Function.uncurry Y ∈
      MvPolynomial.zeroLocus K
        (MvPolynomial.vanishingIdeal k (Function.uncurry '' MulAction.orbit (ConjAct (GL n K)) X)) ↔
    ∀ (j : ℕ), (Y ^ j).rank ≤ (X ^ j).rank
Sources
LeanMatrix.mem_closure_orbit_iff_forall_rank_pow_le · Matrix.mem_zeroLocus_vanishingIdeal_orbit_iff_forall_rank_pow_le

TheoremHadamard's bound, ℓ¹ row form#

The absolute value of a determinant is at most the product of the ℓ¹ norms of the rows.

Matrix.abv_det_le_prod_sum_abv.{u_1, u_2, u_3} {R : Type u_1} {S : Type u_2} [CommRing R]
  [Nontrivial R] [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] {n : Type u_3} [Fintype n]
  [DecidableEq n] (A : Matrix n n R) (abv : AbsoluteValue R S) : abv A.det ≤ ∏ i, ∑ j, abv (A i j)
Lean

Formalized in Tau Ceti as Matrix.abv_det_le_prod_sum_abv.

Other forms

Hadamard's bound, ℓ¹ column form. Formalized in Tau Ceti as Matrix.abv_det_le_prod_sum_abv'.

Matrix.abv_det_le_prod_sum_abv'.{u_1, u_2, u_3} {R : Type u_1} {S : Type u_2} [CommRing R]
  [Nontrivial R] [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] {n : Type u_3} [Fintype n]
  [DecidableEq n] (A : Matrix n n R) (abv : AbsoluteValue R S) : abv A.det ≤ ∏ j, ∑ i, abv (A i j)

Hadamard's bound, ℓ¹ column form, for |·|. Formalized in Tau Ceti as Matrix.abs_det_le_prod_sum_abs'.

Matrix.abs_det_le_prod_sum_abs'.{u_2, u_3} {S : Type u_2} [CommRing S] [LinearOrder S]
  [IsStrictOrderedRing S] {n : Type u_3} [Fintype n] [DecidableEq n] (A : Matrix n n S) :
  |A.det| ≤ ∏ j, ∑ i, |A i j|

Hadamard's bound, ℓ¹ row form, for |·|. Formalized in Tau Ceti as Matrix.abs_det_le_prod_sum_abs.

Matrix.abs_det_le_prod_sum_abs.{u_2, u_3} {S : Type u_2} [CommRing S] [LinearOrder S]
  [IsStrictOrderedRing S] {n : Type u_3} [Fintype n] [DecidableEq n] (A : Matrix n n S) :
  |A.det| ≤ ∏ i, ∑ j, |A i j|
Sources
LeanMatrix.abv_det_le_prod_sum_abv · Matrix.abv_det_le_prod_sum_abv' · Matrix.abs_det_le_prod_sum_abs' · Matrix.abs_det_le_prod_sum_abs
Used by 1
Used byHadamard's bound at ℚ(√2)

TheoremIwasawa's theorem for the projective symplectic group#

In positive rank, the quotient PSp_{2m}(K) of the symplectic group by its centre is simple as soon as Sp_{2m}(K) is perfect.

TauCeti.GLSymplecticFin.isSimpleGroup_quotient_center.{u} {K : Type u} [Field K] {m : ℕ} [NeZero m]
  (h : commutator ↥(TauCeti.GLSymplecticFin m K) = ⊤) :
  IsSimpleGroup (↥(TauCeti.GLSymplecticFin m K) ⧸ Subgroup.center ↥(TauCeti.GLSymplecticFin m K))
Lean

Formalized in Tau Ceti as TauCeti.GLSymplecticFin.isSimpleGroup_quotient_center.

Sources
LeanTauCeti.GLSymplecticFin.isSimpleGroup_quotient_center
Uses 1
Proof usesIwasawa's criterion for a quotient

TheoremJacobi's complementary minor theorem#

For #I = #J = k, the product of the determinant of A and the complementary minor of the adjugate, with rows Jᶜ and columns Iᶜ, is (-1) ^ (∑ I + ∑ J) times (det A) ^ (n - k) times the minor A[I, J].

Matrix.det_mul_det_submatrix_adjugate.{u_1} {R : Type u_1} [CommRing R] {n k : ℕ}
  (A : Matrix (Fin n) (Fin n) R) {I J : Finset (Fin n)} (hI : I.card = k) (hJ : J.card = k) :
  A.det * (A.adjugate.submatrix ⇑(Jᶜ.orderEmbOfFin ⋯) ⇑(Iᶜ.orderEmbOfFin ⋯)).det =
    (-1) ^ (∑ i ∈ I, ↑i + ∑ j ∈ J, ↑j) * A.det ^ (n - k) *
      (A.submatrix ⇑(I.orderEmbOfFin hI) ⇑(J.orderEmbOfFin hJ)).det
Lean

Formalized in Tau Ceti as Matrix.det_mul_det_submatrix_adjugate.

Sources
LeanMatrix.det_mul_det_submatrix_adjugate

TheoremJacobi's complementary-minor identity#

Jacobi's complementary-minor identity for an arbitrary index type n, split into two groups of indices by an equivalence e : m ⊕ p ≃ n.

Matrix.det_submatrix_comp_inr_eq_sign_mul_det_mul_det_submatrix_comp_inl.{u_1, u_2, u_3, u_4}
  {m : Type u_1} {p : Type u_2} {n : Type u_3} {R : Type u_4} [CommRing R] [Fintype m] [Fintype p]
  [DecidableEq m] [DecidableEq p] [Fintype n] [DecidableEq n] (A B : Matrix n n R) (hAB : A * B = 1)
  (e : m ⊕ p ≃ n) (σ τ : Equiv.Perm n) :
  (A.submatrix (⇑τ ∘ ⇑e ∘ Sum.inr) (⇑σ ∘ ⇑e ∘ Sum.inr)).det =
    ↑↑(Equiv.Perm.sign σ) * ↑↑(Equiv.Perm.sign τ) * A.det *
      (B.submatrix (⇑σ ∘ ⇑e ∘ Sum.inl) (⇑τ ∘ ⇑e ∘ Sum.inl)).det
Lean

Formalized in Tau Ceti as Matrix.det_submatrix_comp_inr_eq_sign_mul_det_mul_det_submatrix_comp_inl.

Other forms

Jacobi's complementary-minor identity. Formalized in Tau Ceti as Matrix.det_submatrix_inr_eq_sign_mul_det_mul_det_submatrix_inl.

Matrix.det_submatrix_inr_eq_sign_mul_det_mul_det_submatrix_inl.{u_1, u_2, u_4} {m : Type u_1}
  {p : Type u_2} {R : Type u_4} [CommRing R] [Fintype m] [Fintype p] [DecidableEq m] [DecidableEq p]
  (A B : Matrix (m ⊕ p) (m ⊕ p) R) (hAB : A * B = 1) (σ τ : Equiv.Perm (m ⊕ p)) :
  (A.submatrix (⇑τ ∘ Sum.inr) (⇑σ ∘ Sum.inr)).det =
    ↑↑(Equiv.Perm.sign σ) * ↑↑(Equiv.Perm.sign τ) * A.det *
      (B.submatrix (⇑σ ∘ Sum.inl) (⇑τ ∘ Sum.inl)).det
Sources
LeanMatrix.det_submatrix_comp_inr_eq_sign_mul_det_mul_det_submatrix_comp_inl · Matrix.det_submatrix_inr_eq_sign_mul_det_mul_det_submatrix_inl
Used by 1
Used byJacobi's complementary-minor identity for the two Toeplitz matrices of symmetric polynomials

TheoremJacobi's formula, by rows#

Replacing the i-th row of A by the i-th row of B and summing the determinants over i gives trace (adj A * B), the derivative of det at A in the direction B.

Matrix.sum_det_updateRow_eq_trace_adjugate_mul.{u_1, u_2} {K : Type u_1} [CommRing K] {n : Type u_2}
  [Fintype n] [DecidableEq n] (A B : Matrix n n K) :
  ∑ i, (A.updateRow i (B i)).det = (A.adjugate * B).trace
Lean

Formalized in Tau Ceti as Matrix.sum_det_updateRow_eq_trace_adjugate_mul.

Other forms

Jacobi's formula, by columns. Formalized in Tau Ceti as Matrix.sum_det_updateCol_eq_trace_adjugate_mul.

Matrix.sum_det_updateCol_eq_trace_adjugate_mul.{u_1, u_2} {K : Type u_1} [CommRing K] {n : Type u_2}
  [Fintype n] [DecidableEq n] (A B : Matrix n n K) :
  ∑ j, (A.updateCol j fun i => B i j).det = (A.adjugate * B).trace
Sources
LeanMatrix.sum_det_updateRow_eq_trace_adjugate_mul · Matrix.sum_det_updateCol_eq_trace_adjugate_mul
Used by 1
Used byJacobi's adjugate formula, valid at singular as well as invertible matrices

TheoremPerron–Frobenius theorem for nonnegative matrices#

an entrywise nonnegative real square matrix has its spectral radius r, viewed as a complex matrix, as an eigenvalue, with an eigenvector whose entries are nonnegative and not all zero.

Unlike the strictly positive and irreducible cases (Matrix.exists_mulVec_eq_smul_of_pos and Matrix.IsIrreducible.exists_mulVec_eq_smul), the eigenvector may have zero entries and need not be unique up to scalars, and r may be zero.

Matrix.exists_mulVec_eq_smul_of_nonneg.{u_1} {n : Type u_1} [Fintype n] {A : Matrix n n ℝ}
  [Nonempty n] (hA : ∀ (i j : n), 0 ≤ A i j) :
  ∃ r,
    0 ≤ r ∧
      spectralRadius ℂ (A.map Complex.ofReal) = ENNReal.ofReal r ∧
        ∃ v, 0 ≤ v ∧ v ≠ 0 ∧ A.mulVec v = r • v
Informally uses
Lean

Formalized in Tau Ceti as Matrix.exists_mulVec_eq_smul_of_nonneg.

Other forms

Perron–Frobenius. Formalized in Tau Ceti as Matrix.IsIrreducible.rootMultiplicity_charpoly_eq_one.

Matrix.IsIrreducible.rootMultiplicity_charpoly_eq_one.{u_1} {n : Type u_1} [Fintype n]
  {A : Matrix n n ℝ} {v : n → ℝ} {r : ℝ} [DecidableEq n] [Nonempty n] (hA : A.IsIrreducible)
  (hv : ∀ (i : n), 0 < v i) (hAv : A.mulVec v = r • v) :
  Polynomial.rootMultiplicity r A.charpoly = 1

Perron–Frobenius. Formalized in Tau Ceti as Matrix.IsPrimitive.eq_of_norm_eq_of_mulVec_eq_smul.

Matrix.IsPrimitive.eq_of_norm_eq_of_mulVec_eq_smul.{u_1} {n : Type u_1} [Fintype n] [DecidableEq n]
  {A : Matrix n n ℝ} {v : n → ℝ} {r : ℝ} {μ : ℂ} (hA : A.IsPrimitive) (hv : ∀ (i : n), 0 < v i)
  (hAv : A.mulVec v = r • v) {z : n → ℂ} (hz : z ≠ 0)
  (hAz : (A.map Complex.ofReal).mulVec z = μ • z) (hμ : ‖μ‖ = r) : μ = ↑r

Perron–Frobenius. Formalized in Tau Ceti as Matrix.IsPrimitive.norm_lt_of_mem_spectrum.

Matrix.IsPrimitive.norm_lt_of_mem_spectrum.{u_1} {n : Type u_1} [Fintype n] [DecidableEq n]
  {A : Matrix n n ℝ} {v : n → ℝ} {r : ℝ} {μ : ℂ} (hA : A.IsPrimitive) (hv : ∀ (i : n), 0 < v i)
  (hAv : A.mulVec v = r • v) (hμ : μ ∈ spectrum ℂ (A.map Complex.ofReal)) (hμr : μ ≠ ↑r) : ‖μ‖ < r

Perron–Frobenius. Formalized in Tau Ceti as Matrix.IsPrimitive.norm_lt_of_mulVec_eq_smul.

Matrix.IsPrimitive.norm_lt_of_mulVec_eq_smul.{u_1} {n : Type u_1} [Fintype n] [DecidableEq n]
  {A : Matrix n n ℝ} {v : n → ℝ} {r : ℝ} {μ : ℂ} (hA : A.IsPrimitive) (hv : ∀ (i : n), 0 < v i)
  (hAv : A.mulVec v = r • v) {z : n → ℂ} (hz : z ≠ 0)
  (hAz : (A.map Complex.ofReal).mulVec z = μ • z) (hμ : μ ≠ ↑r) : ‖μ‖ < r

Perron–Frobenius. Formalized in Tau Ceti as Matrix.eq_of_norm_eq_of_mulVec_eq_smul.

Matrix.eq_of_norm_eq_of_mulVec_eq_smul.{u_1} {n : Type u_1} [Fintype n] {A : Matrix n n ℝ}
  {v : n → ℝ} {r : ℝ} (hA : ∀ (i j : n), 0 < A i j) (hv : ∀ (i : n), 0 < v i)
  (hAv : A.mulVec v = r • v) {μ : ℂ} {z : n → ℂ} (hz : z ≠ 0)
  (hAz : (A.map Complex.ofReal).mulVec z = μ • z) (hμ : ‖μ‖ = r) : μ = ↑r

Perron–Frobenius. Formalized in Tau Ceti as Matrix.spectralRadius_eq_of_mulVec_eq_smul.

Matrix.spectralRadius_eq_of_mulVec_eq_smul.{u_1} {n : Type u_1} [Fintype n] {A : Matrix n n ℝ}
  {v : n → ℝ} {r : ℝ} [Nonempty n] (hA : ∀ (i j : n), 0 ≤ A i j) (hv : ∀ (i : n), 0 < v i)
  (hAv : A.mulVec v = r • v) : spectralRadius ℂ (A.map Complex.ofReal) = ENNReal.ofReal r

Perron–Frobenius theorem for irreducible matrices, existence. Formalized in Tau Ceti as Matrix.IsIrreducible.exists_mulVec_eq_smul.

Matrix.IsIrreducible.exists_mulVec_eq_smul.{u_1} {n : Type u_1} [Fintype n] {A : Matrix n n ℝ}
  [Nonempty n] (hA : A.IsIrreducible) : ∃ r, 0 < r ∧ ∃ v, (∀ (i : n), 0 < v i) ∧ A.mulVec v = r • v

Perron–Frobenius theorem for positive matrices, existence. Formalized in Tau Ceti as Matrix.exists_mulVec_eq_smul_of_pos.

Matrix.exists_mulVec_eq_smul_of_pos.{u_1} {n : Type u_1} [Fintype n] {A : Matrix n n ℝ} [Nonempty n]
  (hA : ∀ (i j : n), 0 < A i j) : ∃ r, 0 < r ∧ ∃ v, (∀ (i : n), 0 < v i) ∧ A.mulVec v = r • v
Sources
LeanMatrix.exists_mulVec_eq_smul_of_nonneg · Matrix.IsIrreducible.rootMultiplicity_charpoly_eq_one · Matrix.IsPrimitive.eq_of_norm_eq_of_mulVec_eq_smul · Matrix.IsPrimitive.norm_lt_of_mem_spectrum · Matrix.IsPrimitive.norm_lt_of_mulVec_eq_smul · Matrix.eq_of_norm_eq_of_mulVec_eq_smul · Matrix.spectralRadius_eq_of_mulVec_eq_smul · Matrix.IsIrreducible.exists_mulVec_eq_smul · Matrix.exists_mulVec_eq_smul_of_pos
Used by 3
Used byTauCeti.SplitK0.spectralRadius_fusionMatrix · The Frobenius–Perron character · Collatz–Wielandt bound

TheoremSherman–Morrison formula over a commutative ring#

The rank-one correction is the outer product of the updated column and row, divided by the scalar denominator.

Matrix.inv_add_vecMulVec.{u_1, u_2} {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n]
  [CommRing R] (A : Matrix n n R) (hA : IsUnit A) (u v : n → R)
  (hd : IsUnit (1 + v ⬝ᵥ A⁻¹.mulVec u)) :
  (A + Matrix.vecMulVec u v)⁻¹ =
    A⁻¹ -
      Ring.inverse (1 + v ⬝ᵥ A⁻¹.mulVec u) • Matrix.vecMulVec (A⁻¹.mulVec u) (Matrix.vecMul v A⁻¹)
Lean

Formalized in Tau Ceti as Matrix.inv_add_vecMulVec.

Sources
LeanMatrix.inv_add_vecMulVec

TheoremSkolem–Noether for matrix algebras over a local semiring#

every algebra automorphism of a matrix algebra over a commutative local semiring, in particular over a field, is inner.

Matrix.GeneralLinearGroup.innerAut_surjective.{u_1, u_2} {n : Type u_1} [Fintype n] [DecidableEq n]
  (K : Type u_2) [CommSemiring K] [IsLocalRing K] :
  Function.Surjective ⇑Matrix.GeneralLinearGroup.innerAut
Lean

Formalized in Tau Ceti as Matrix.GeneralLinearGroup.innerAut_surjective.

Sources
LeanMatrix.GeneralLinearGroup.innerAut_surjective
Used by 2
Used bySpin₅ is a twisted form of Sp₄ · Split Spin₅ is Sp₄

TheoremSylvester's rank inequality#

for an m × n matrix A and an n × o matrix B over a field, rank A + rank B ≤ rank (A * B) + n. Equivalently, multiplying by A lowers the rank of B by at most the nullity of A.

Matrix.rank_add_rank_le_rank_mul_add_card.{u_1, u_2, u_3, u_4} {K : Type u_1} [Field K]
  {m : Type u_2} {n : Type u_3} [Fintype n] {o : Type u_4} [Fintype o] (A : Matrix m n K)
  (B : Matrix n o K) : A.rank + B.rank ≤ (A * B).rank + Fintype.card n
Lean

Formalized in Tau Ceti as Matrix.rank_add_rank_le_rank_mul_add_card.

Sources
LeanMatrix.rank_add_rank_le_rank_mul_add_card
Used by 1
Used byPrime torsion of a numerical type

TheoremUltrametric Hadamard bound, row form#

For a nonarchimedean absolute value abv, if row i of A is bounded entrywise in abv by b i, then abv A.det ≤ ∏ i, b i.

Matrix.abv_det_le_prod_of_le.{u_1, u_2, u_3} {R : Type u_1} {S : Type u_2} [CommRing R]
  [Nontrivial R] [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] {n : Type u_3} [Fintype n]
  [DecidableEq n] (A : Matrix n n R) {abv : AbsoluteValue R S} (habv : IsNonarchimedean ⇑abv)
  {b : n → S} (hA : ∀ (i j : n), abv (A i j) ≤ b i) : abv A.det ≤ ∏ i, b i
Lean

Formalized in Tau Ceti as Matrix.abv_det_le_prod_of_le.

Other forms

Ultrametric Hadamard bound, column form. Formalized in Tau Ceti as Matrix.abv_det_le_prod_of_le'.

Matrix.abv_det_le_prod_of_le'.{u_1, u_2, u_3} {R : Type u_1} {S : Type u_2} [CommRing R]
  [Nontrivial R] [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] {n : Type u_3} [Fintype n]
  [DecidableEq n] (A : Matrix n n R) {abv : AbsoluteValue R S} (habv : IsNonarchimedean ⇑abv)
  {b : n → S} (hA : ∀ (i j : n), abv (A i j) ≤ b j) : abv A.det ≤ ∏ j, b j
Sources
LeanMatrix.abv_det_le_prod_of_le · Matrix.abv_det_le_prod_of_le'

TheoremWhitehead's lemma#

For an invertible matrix u, the block diagonal matrix u ⊕ u⁻¹ is elementary: it is the product of six block unipotent matrices, u ⊕ u⁻¹ = U(u) L(-u⁻¹) U(u) U(-1) L(1) U(-1).

TauCeti.fromBlocksGL_inv_mem_elementarySubgroup.{u_1, u_2} {A : Type u_1} [Ring A] {m : Type u_2}
  [DecidableEq m] [Fintype m] (u : GL m A) :
  TauCeti.fromBlocksGL (u, u⁻¹) ∈ TauCeti.elementarySubgroup (m ⊕ m) A
Lean

Formalized in Tau Ceti as TauCeti.fromBlocksGL_inv_mem_elementarySubgroup.

Sources
LeanTauCeti.fromBlocksGL_inv_mem_elementarySubgroup

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.