Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-25 17:43 374885af

View on Github →

feat(linear_algebra/matrix/nonsingular_inverse): lemmas about adjugate (#9947)

Estimated changes

Modified src/linear_algebra/matrix/determinant.lean

added theorem matrix.det_update_column_smul'

added theorem matrix.det_update_row_smul'

Modified src/linear_algebra/matrix/nonsingular_inverse.lean

added theorem matrix.adjugate_conj_transpose

added theorem matrix.adjugate_smul

added theorem matrix.cramer_smul

deleted theorem matrix.ring_hom.map_adjugate

added theorem ring_hom.map_adjugate

Modified src/linear_algebra/multilinear/basic.lean

added theorem multilinear_map.map_update_smul