determinant): generalize det_fin_zero to det_eq_one_of_is_empty (#8387)

Commit

4 years ago

feat(linear_algebra/matrix/determinant): generalize det_fin_zero to det_eq_one_of_is_empty (#8387) Also golfs a nearby proof

Author

eric-wieser

Parents