Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-29 00:33 bdcb7310

View on Github →

feat(linear_algebra/matrix/adjugate): det_adjugate and adjugate_adjugate (#9991) This also adds matrix.mv_polynomial_X

Estimated changes

Modified src/linear_algebra/matrix/adjugate.lean

added theorem alg_hom.map_adjugate

added theorem matrix.adjugate_adjugate'

added theorem matrix.adjugate_adjugate

added theorem matrix.det_adjugate

deleted theorem matrix.det_adjugate_eq_one

deleted theorem matrix.det_adjugate_of_cancel

deleted theorem matrix.det_adjugate_of_is_unit

added theorem matrix.det_smul_adjugate_adjugate

Created src/linear_algebra/matrix/mv_polynomial.lean

added theorem matrix.det_mv_polynomial_X_ne_zero

added theorem matrix.mv_polynomial_X_map_eval₂

added theorem matrix.mv_polynomial_X_map_matrix_aeval

added theorem matrix.mv_polynomial_X_map_matrix_eval

Modified src/linear_algebra/special_linear_group.lean