A cofactor row by row replacement

MathlibAnnex.Piola.cofactorRow

def

Fixes the cofactor convention used in the divergence and determinant identities.

Statement

Let be a real matrix, and fix a row index . Write for the th coordinate vector. The cofactor row is the vector whose th coordinate is the determinant obtained by replacing row of by .

Definition

For a row vector , let denote with only its th row replaced by . Then Equivalently, is the usual cofactor. The row-replacement formula fixes the row and column convention without choosing an inverse.

Assumptions

The matrix is arbitrary: invertibility is not required. The dimension is a natural number, with a specified . When there is no such index, so this indexed definition has no instance to evaluate.

Conclusion

The result is a row in , using the row convention throughout. No transpose or choice of an inverse is part of the definition.

The later row-expansion lemma gives . It is cited as a separate identity, not included as an additional conclusion of this definition.

def cofactorRow {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ)
    (i : Fin n) : (Fin n → ℝ) :=
  fun j => (A.updateRow i (basisRow j)).det

noncomputable section

open scoped BigOperators

namespace MathlibAnnex
namespace Piola

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project