Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-25 11:18 75e07d1c

View on Github →

feat(linear_algebra/matrix/determinant): lemmas about commutativity under det (#7685)

Estimated changes

Modified src/linear_algebra/matrix/determinant.lean

added theorem matrix.det_mul_comm

added theorem matrix.det_mul_left_comm

added theorem matrix.det_mul_right_comm

added theorem matrix.det_units_conj'

added theorem matrix.det_units_conj