Commit 2020-07-14 01:25 04109461

View on Github →

chore(linear_algebra/nonsingular_inverse): swap update_row/column names (#3393) The names for update_row and update_column did not correspond to their definitions. Doing a global swap of the names keep all the proofs valid and makes the semantics match.

Estimated changes

Modified src/linear_algebra/nonsingular_inverse.lean

modified theorem matrix.cramer_apply

modified def matrix.cramer_map

modified def matrix.update_column

modified theorem matrix.update_column_ne

modified theorem matrix.update_column_self

deleted theorem matrix.update_column_transpose

modified theorem matrix.update_column_val

modified def matrix.update_row

modified theorem matrix.update_row_ne

modified theorem matrix.update_row_self

added theorem matrix.update_row_transpose

modified theorem matrix.update_row_val