Commit 2026-07-19 02:25 c2ea7ca1

View on Github →

feat: add theorem that Bird's determinant algorithm computes Matrix.det (#41160) This PR adds:

theorem det_eq_birdDet {n : Nat} (A : Array R) (hA : A.size = n * n) :
    Matrix.det (Matrix.ofArray (m := n) (n := n) A hA) = birdDet n A

showing that Bird's determinant algorithm computes Matrix.det. The PR also adds:

  • BirdDet.Spec.birdDet - an alternative implementation of Bird's algorithm that's stated in terms of Matrix instead of Array.

Estimated changes

added theorem Fin.cons_comp_succ
added theorem Fin.cons_zero_succ
added theorem Fin.range_insertNth
added def BirdDet.S
added theorem BirdDet.S_zero
added theorem BirdDet.mem_S_iff
added theorem BirdDet.paper_eq1
added theorem BirdDet.paper_eq2
added theorem BirdDet.paper_eq3
added theorem BirdDet.paper_eq5
modified def BirdDet.birdDet
added theorem BirdDet.birdDet_succ
modified theorem BirdDet.birdDet_zero
added theorem BirdDet.get_eq
deleted theorem BirdDet.iter_succ
deleted theorem BirdDet.iter_zero
added theorem BirdDet.stepEntry_eq
added theorem BirdDet.sumFrom_induct
added theorem Fin.liftFun_cons
added theorem Fin.strictMono_cons
added theorem StrictMono.removeNth