Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-23 08:42 11a365de

View on Github →

feat(linear_algebra/matrix): add variants of the existing det_units_conj lemmas (#12881)

Estimated changes

Modified src/linear_algebra/determinant.lean

deleted theorem matrix.det_conj

added theorem matrix.det_conj_of_mul_eq_one

Modified src/linear_algebra/matrix/nonsingular_inverse.lean

added theorem matrix.coe_units_inv

added theorem matrix.det_conj'

added theorem matrix.det_conj

Modified src/linear_algebra/matrix/zpow.lean

added theorem matrix.coe_units_zpow

deleted theorem matrix.units.coe_inv''

deleted theorem matrix.units.coe_zpow