Commit 2021-10-25 17:43 87fa12a7
View on Github →chore(linear_algebra/matrix/nonsingular_inverse): replace 1 < fintype.card n with nontrivial n (#9953)
This likely makes this a better simp lemma
chore(linear_algebra/matrix/nonsingular_inverse): replace 1 < fintype.card n with nontrivial n (#9953)
This likely makes this a better simp lemma