Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-01 00:19 802c5b5a

View on Github →

feat(linear_algebra/determinant): various operations preserve the determinant (#7115) These are a couple of helper lemmas for computing the determinant of a Vandermonde matrix.

Estimated changes

Modified src/data/matrix/basic.lean

added theorem matrix.update_column_eq_self

added theorem matrix.update_row_eq_self

Modified src/linear_algebra/determinant.lean

added theorem matrix.det_eq_of_eq_det_one_mul

added theorem matrix.det_eq_of_eq_mul_det_one

added theorem matrix.det_eq_of_forall_col_eq_smul_add_pred

added theorem matrix.det_eq_of_forall_row_eq_smul_add_const

added theorem matrix.det_eq_of_forall_row_eq_smul_add_const_aux

added theorem matrix.det_eq_of_forall_row_eq_smul_add_pred

added theorem matrix.det_eq_of_forall_row_eq_smul_add_pred_aux

added theorem matrix.det_mul_column

added theorem matrix.det_mul_row

added theorem matrix.det_update_column_add_self

added theorem matrix.det_update_column_add_smul_self

added theorem matrix.det_update_row_add_self

added theorem matrix.det_update_row_add_smul_self

added theorem matrix.det_zero_of_column_eq