mathlib

1d183094 - feat(linear_algebra/determinant): no need for `is_domain` (#12805)

feat(linear_algebra/determinant): no need for `is_domain` (#12805) Nontriviality is all that was actually used, and in some cases the statement is already vacuous in the trivial case.