Matrix determinant lemma

TheoremMatrix determinant lemma without invertibility#✓fully proved

The matrix determinant lemma, without any invertibility hypothesis: the determinant of a rank-one update of A is det A plus the adjugate pairing v ⬝ᵥ (adjugate A *ᵥ u). This is the general version left as a TODO in Mathlib's Matrix.det_add_replicateCol_mul_replicateRow.

theorem det_add_vecMulVec (A : Matrix n n R) (u v : n → R) :
    (A + vecMulVec u v).det = A.det + v ⬝ᵥ (adjugate A *ᵥ u)

Used by 3

Used byMatrix determinant lemma in column-times-row form · Multiplicative matrix determinant lemma for invertible matrices · Invertibility criterion for a rank-one update

TheoremMatrix determinant lemma in column-times-row form#✓fully proved

The matrix determinant lemma in the replicateCol / replicateRow form stated in Mathlib's TODO for Matrix.det_add_replicateCol_mul_replicateRow. The _general suffix avoids clashing with Mathlib's invertible version of the same name.

theorem det_add_replicateCol_mul_replicateRow_general {ι : Type*} [Unique ι]
    (A : Matrix n n R) (u v : n → R) :
    (A + replicateCol ι u * replicateRow ι v).det =
      A.det + v ⬝ᵥ (adjugate A *ᵥ u)

Uses 1

Proof usesMatrix determinant lemma without invertibility

TheoremInvertibility criterion for a rank-one update#✓fully proved

A rank-one update of A is a unit exactly when the adjugate correction term is a unit; no invertibility hypothesis on A is needed.

theorem isUnit_add_vecMulVec_iff (A : Matrix n n R) (u v : n → R) :
    IsUnit (A + vecMulVec u v) ↔
      IsUnit (A.det + v ⬝ᵥ (adjugate A *ᵥ u))

Uses 1

Proof usesMatrix determinant lemma without invertibility

TheoremMultiplicative matrix determinant lemma for invertible matrices#✓fully proved

The matrix determinant lemma in multiplicative form, when A.det is a unit: this recovers Mathlib's Matrix.det_add_replicateCol_mul_replicateRow from the general version.

theorem det_add_vecMulVec_of_isUnit_det (A : Matrix n n R) (u v : n → R)
    (hA : IsUnit A.det) :
    (A + vecMulVec u v).det = A.det * (1 + v ⬝ᵥ A⁻¹ *ᵥ u)

Uses 1

Proof usesMatrix determinant lemma without invertibility

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.