Theorem BirdDet.det_submatrix_removeNth_eq_sign_mul_bminor

Modification history

2026-07-19 02:25
Mathlib/LinearAlgebra/Matrix/Determinant/Bird/Correctness.lean
feat: add theorem that Bird's determinant algorithm computes Matrix.det (#41160) …
Added BirdDet.det_submatrix_removeNth_eq_sign_mul_bminorView on Github →