Cauchy Binet theorem

Stream: Is there code for X?

[Yufei Liu]

Has Cauchy Binet theorem been formalised in LEAN? how close are we?

[Kevin Buzzard]

guessing docs#Matrix.det_mul

[Kevin Buzzard]

Oh -- this is not the theorem, so maybe not?

[Kevin Buzzard]

I guess even formalising the statement will be an interesting exercise.

[Yufei Liu]

Kevin Buzzard said:

I guess even formalising the statement will be an interesting exercise.

I see, thank you for your reply!

[Eric Wieser]

Here's such a statement, which was indeed interesting!

import Mathlib

variable {m n R : Type*}

-- This probably belongs in mathlib
instance : MulAction (Equiv.Perm m)ᵈᵐᵃ (m ↪ n) where
  smul σ f := (DomAddAct.mk.symm σ).toEmbedding.trans f
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

@[simp]
theorem DomMulAct.equivPerm_smul_embedding_def (σ : Equiv.Perm m) (f : m ↪ n) :
    DomMulAct.mk σ • f = σ.toEmbedding.trans f := rfl

/-- A choice of `m` elements of `n`. -/
abbrev Function.Embedding.ModPerm (m n : Type*) : Type _ :=
  -- or could build the quotient manually
  MulAction.orbitRel.Quotient (Equiv.Perm m)ᵈᵐᵃ (m ↪ n)

variable [Fintype m] [Fintype n]

-- this is a hack, a decidable algorithm would be better!
noncomputable instance : Fintype (Function.Embedding.ModPerm m n) := by
  classical exact Quotient.fintype _

variable [DecidableEq m] [CommRing R]

open Nat

/-- Cauchy-Binet, https://en.wikipedia.org/wiki/Cauchy%E2%80%93Binet_formula -/
theorem Matrix.det_mul' (A : Matrix m n R) (B : Matrix n m R) :
    det (A * B) = ∑ f : Function.Embedding.ModPerm m n,
      f.liftOn
        (fun f => det (A.submatrix id f) * det (B.submatrix f id))
        (by
          rintro f g ⟨σ, rfl⟩; revert σ; rw [DomMulAct.mk.surjective.forall]; intro σ
          show (A.submatrix id ⇑g |>.submatrix id ⇑σ).det * (B.submatrix g id |>.submatrix σ id).det = (A.submatrix id ⇑g).det * (B.submatrix (⇑g) id).det
          rw [det_permute', det_permute, mul_mul_mul_comm]
          rw [← Int.cast_mul, Int.units_coe_mul_self, Int.cast_one, one_mul]) := by
  -- real proof starts here
  sorry

[Notification Bot]

A message was moved here from #Is there code for X? > Minors of matrices (square and non-square) by Eric Wieser.