Theorem Matrix.detp_one_diagonal

Modification history

2026-02-23 13:05
Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean
chore(LinearAlgebra/Matrix/SemiringInverse): generalize from the identity to diagonal matrices (#35676) …
Added Matrix.detp_one_diagonalView on Github →