MATHLIBANNEX / CANONICAL DECLARATION CARD

A unique right factor from proportional oriented maximal minors

MathlibAnnex.Matrix.existsUnique_factor_of_orientedMaximalMinorsProportional

theorem

Recovers a square factor and its determinant from proportional determinants of every ordered row tuple.

Statement

Let be -by- matrices over a field and let . For an ordered tuple , let be the selected square matrices, retaining the order and any repetitions in . Assume

Suppose one tuple satisfies . There is a unique square matrix with and .

Assumptions

The coefficient system is any field; is any set, without an order or finiteness assumption. The scalar is nonzero, proportionality holds for all ordered tuples, and the same chosen tuple supplies the nonzero minor. The case is included.

Conclusion

Writing and , the factor is

It satisfies and , hence is invertible. The uniqueness already follows from .

Notes

If has a linear order, proportionality of the increasing-row minor families implies the ordered-tuple hypothesis: sorting an injective tuple introduces the same permutation sign for both matrices, while a repeated row makes both determinants zero. This adapter is separate from the theorem’s order-free assumptions. A nonzero selected minor also implies that multiplication by on column vectors is injective: restrict to the selected rows and multiply by .

Proof route

Use the same nonzero selected minor to compare every row’s coordinates by Cramer’s rule. The coordinate equality supplies the global factorization; the selected square equation supplies its determinant and uniqueness.

Proof steps

  1. Proportionality at gives . Since and are nonzero in a field, . Thus both and are invertible. Define ; immediately .

  2. Fix any row index and write for the corresponding rows. For every position , replace the th entry of by . The hypothesis applies even if this creates a repeated entry. The selected matrices are and , so Cramer’s row formula gives

    Cancellation of proves .

  3. Multiply the last row identity on the right by :

    It holds for every , hence . Taking determinants in the selected equation gives ; canceling the nonzero factor yields .

  4. If another matrix satisfies , selecting the same rows gives . Multiplication by forces . This proves uniqueness even before imposing the determinant condition.

  5. To pass from increasing minors to arbitrary tuples when an order on is available, write an injective tuple as an increasing enumeration composed with a permutation . Both determinants gain the factor , so their proportionality is unchanged. A noninjective tuple has two equal rows and both determinants vanish. For , there is one empty tuple, both determinants are , and the hypothesis reads , forcing ; the unique empty matrix is the required factor.

Main citations

Lean source signature (exact)

theorem existsUnique_factor_of_orientedMaximalMinorsProportional
    {n : ℕ} {ι : Type u} {K : Type v} [Field K]
    (source target : _root_.Matrix ι (Fin n) K) (scale : K)
    (hscale : scale ≠ 0)
    (hminor : OrientedMaximalMinorsProportional source target scale)
    (rows : Fin n → ι)
    (htarget : orientedMaximalMinor target rows ≠ 0) :
    ∃! L : _root_.Matrix (Fin n) (Fin n) K,
      target * L = source ∧ L.det = scale
In the source Mathematical meaning
{n : ℕ} {ι : Type u} {K : Type v} [Field K] , any row set and any coefficient field. No order or finiteness of is assumed.
(source target : root.Matrix ι (Fin n) K) (scale : K) The two matrices and scalar , respectively; thus target * L = source means .
(hscale : scale ≠ 0) The hypothesis .
(hminor : OrientedMaximalMinorsProportional source target scale) For every ordered tuple , . The cited definition retains the tuple order, including repetitions.
In the source Mathematical meaning
(rows : Fin n → ι) (htarget : orientedMaximalMinor target rows ≠ 0) The chosen tuple and the hypothesis . The same chosen rows form and .
∃! L : root.Matrix (Fin n) (Fin n) K, target * L = source ∧ L.det = scale There is exactly one square matrix satisfying both and . Its formula in the conclusion is . The case is included.
Exact surrounding binder context (separate excerpt) 
noncomputable section

open scoped Matrix

namespace MathlibAnnex
namespace Matrix

universe u v

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

Exact content identity

Declaration: MathlibAnnex.Matrix.existsUnique_factor_of_orientedMaximalMinorsProportional

Accepted content SHA-256: ee813a627f4b80001e5edf28439adb3034b15e6c5c1f0c8306a3e0164e66cf6e

Accepted source guide SHA-256: c465f63f209d9fa55fd71e5d2c19abf7e285f8574f16a90f907281ed6df239b4

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑