Theorem BirdDet.iter_succ

Modification history

2026-07-19 02:25
Mathlib/LinearAlgebra/Matrix/Determinant/Bird/Defs.lean
feat: add theorem that Bird's determinant algorithm computes Matrix.det (#41160) …
Deleted BirdDet.iter_succView on Github →
2026-07-02 19:14
Mathlib/LinearAlgebra/Matrix/Determinant/Bird.lean
feat: add normalization simproc for Bird's determinant algorithm (#41158) …
Added BirdDet.iter_succView on Github →