Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-22 07:48 fb5ef2b9

View on Github →

feat(linear_algebra/nonsingular_inverse): state Cramer's rule explicitly (#4700) Mostly so that we can add an entry to the Freek 100.

Estimated changes

Modified docs/100.yaml

Modified src/data/matrix/basic.lean

added theorem matrix.smul_mul_vec_assoc

Modified src/linear_algebra/determinant.lean

modified theorem matrix.det_eq_zero_of_column_eq_zero

added theorem matrix.det_eq_zero_of_row_eq_zero

deleted theorem matrix.det_zero_of_column_eq

added theorem matrix.det_zero_of_row_eq

Modified src/linear_algebra/nonsingular_inverse.lean

modified def matrix.adjugate

modified def matrix.cramer

modified theorem matrix.cramer_apply

deleted theorem matrix.cramer_column_self

modified def matrix.cramer_map

added theorem matrix.cramer_transpose_eq_adjugate_mul_vec

added theorem matrix.cramer_transpose_row_self

added theorem matrix.cramers_rule