Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-22 14:04 a971a88f

View on Github →

refactor(linear_algebra/nonsingular_inverse, data/matrix/basic): update_* rectangular matrices (#3403)

Estimated changes

Modified src/data/matrix/basic.lean

added def matrix.update_column

added theorem matrix.update_column_ne

added theorem matrix.update_column_self

added theorem matrix.update_column_transpose

added theorem matrix.update_column_val

added def matrix.update_row

added theorem matrix.update_row_ne

added theorem matrix.update_row_self

added theorem matrix.update_row_transpose

added theorem matrix.update_row_val

Modified src/linear_algebra/nonsingular_inverse.lean

deleted def matrix.update_column

deleted theorem matrix.update_column_ne

deleted theorem matrix.update_column_self

deleted theorem matrix.update_column_val

deleted def matrix.update_row

deleted theorem matrix.update_row_ne

deleted theorem matrix.update_row_self

deleted theorem matrix.update_row_transpose

deleted theorem matrix.update_row_val