Commit 2022-03-19 11:33 1d183094

View on Github →

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.

Estimated changes

Modified src/linear_algebra/determinant.lean

modified def equiv_of_pi_lequiv_pi

modified theorem linear_equiv.det_mul_det_symm

modified theorem linear_equiv.det_symm_mul_det

modified theorem linear_equiv.is_unit_det'

modified theorem linear_map.is_unit_det

modified theorem matrix.det_comm'

modified theorem matrix.det_conj

modified def matrix.index_equiv_of_inv

Modified src/linear_algebra/matrix/to_linear_equiv.lean

Modified src/linear_algebra/orientation.lean

modified theorem basis.map_orientation_eq_det_inv_smul

Modified src/ring_theory/norm.lean

modified theorem algebra.norm_eq_zero_iff_of_basis

modified theorem algebra.norm_ne_zero_iff_of_basis

Modified src/topology/algebra/module/basic.lean