Commit 2026-07-02 19:14 2dd99942

feat: add normalization simproc for Bird's determinant algorithm (#41158) add birdDet, an implementation of a division-free determinant algorithm 1, and norm_det / eval_det frontend for normalizing expressions that use birdDet. The algorithm can be used for matrices with symbolic entries over a CommRing (see example below). The normalizer uses the ring tactic's normalisation infrastructure to produce a certificate chain between the birdDet expression and the computed determinant. I chose this particular algorithm because it is efficient enough to work with ~10x10 matrices, and is division-free and so can work with matrices with elements in a general commutative ring. For example:

example {R: Type*} [CommRing R] (a b c d : R) :
    birdDet 2 #[a, b, c, d] = a * d - b * c := by
  simp only [norm_det]
  ring