Commit 2020-10-19 10:38 ef9d00f7

View on Github →

feat(linear_algebra/matrix): multiplying is_basis.to_matrix and linear_map.to_matrix (#4650) This basically tells us that is_basis.to_matrix is indeed a basis change matrix.

Estimated changes

Modified src/linear_algebra/matrix.lean

added theorem is_basis.sum_to_matrix_smul_self

added theorem is_basis.to_lin_to_matrix

modified def is_basis.to_matrix

added theorem is_basis.to_matrix_eq_to_matrix_constr

modified theorem is_basis.to_matrix_self

modified theorem is_basis.to_matrix_update

added theorem is_basis_to_matrix_mul_linear_map_to_matrix

added theorem linear_map_to_matrix_mul_is_basis_to_matrix

added theorem matrix.to_lin_self