Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-25 17:43 5fcbd2b9

View on Github →

chore(linear_algebra/matrix/nonsingular_inverse): use pi.single instead of ite (#9944)

Estimated changes