Commit 2022-03-31 14:15 25ef4f0f

View on Github →

feat(topology/algebra/matrix): more continuity lemmas for matrices (#13009) This should cover all the definitions in data/matrix/basic, and also picks out a few notable definitions (det, trace, adjugate, cramer, inv) from other files.

Estimated changes

Modified src/analysis/normed_space/finite_dimension.lean

Modified src/topology/algebra/matrix.lean

added theorem continuous.matrix_adjugate

added theorem continuous.matrix_col

added theorem continuous.matrix_cramer

added theorem continuous.matrix_det

added theorem continuous.matrix_diag

added theorem continuous.matrix_dot_product

added theorem continuous.matrix_elem

added theorem continuous.matrix_map

added theorem continuous.matrix_minor

added theorem continuous.matrix_mul

added theorem continuous.matrix_mul_vec

added theorem continuous.matrix_reindex

added theorem continuous.matrix_row

added theorem continuous.matrix_trace

added theorem continuous.matrix_transpose

added theorem continuous.matrix_update_column

added theorem continuous.matrix_update_row

added theorem continuous.matrix_vec_mul

added theorem continuous.matrix_vec_mul_vec

added theorem continuous_at_matrix_inv

deleted theorem continuous_det

added theorem continuous_matrix.diagonal

added theorem continuous_matrix

Modified src/topology/continuous_on.lean

added theorem continuous.if_const