Right multiplication scales every maximal minor by one determinant

MathlibAnnex.Matrix.maximalMinors_mul

theorem

Turns a square right factor into a common scalar on the family of maximal minors.

Statement

For an -by- matrix and an -by- matrix over a commutative ring, with linearly ordered, write for the family of determinants of all -row submatrices in increasing row order. Then

The equality is pointwise on -element row subsets, using increasing row order on both sides.

Assumptions

The integer may be zero; the row set may be infinite. The coefficient ring is commutative. The square factor need not be invertible.

Conclusion

For each selected subset , . Thus one scalar, independent of , scales the whole family.

Related identities in the same source distinguish scalar multiplication from right multiplication: . The zero-matrix family vanishes when ; this restriction matters, because the empty determinant for is . Selection commutes also with application to a column vector: . These are separate identities, not invertibility assumptions for the displayed theorem.

Proof route

Select the same rows before and after multiplication, then apply multiplicativity of the square determinant.

theorem maximalMinors_mul
    {n : ℕ} {ι : Type u} {R : Type v} [LinearOrder ι] [CommRing R]
    (A : _root_.Matrix ι (Fin n) R)
    (L : _root_.Matrix (Fin n) (Fin n) R) :
    maximalMinors (A * L) = L.det • maximalMinors A

noncomputable section

open scoped BigOperators

namespace MathlibAnnex
namespace Matrix

universe u v

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