nonsingular_inverse): replace `1 < fintype.card n` with `nontrivial n` (#9953)

Commit

4 years ago

chore(linear_algebra/matrix/nonsingular_inverse): replace `1 < fintype.card n` with `nontrivial n` (#9953) This likely makes this a better simp lemma

Author

eric-wieser

Parents