Theorem Fin.strictMono_insertNth_iff

Modification history

2026-07-19 02:25
Mathlib/Order/Fin/Tuple.lean
feat: add theorem that Bird's determinant algorithm computes Matrix.det (#41160) …
Added Fin.strictMono_insertNth_iffView on Github →