Commit 2023-04-26 07:58 94f2b209

View on Github →

feat: port Topology.Instances.Matrix (#3655)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Instances/Matrix.lean

added theorem Continuous.matrix_adjugate

added theorem Continuous.matrix_blockDiag'

added theorem Continuous.matrix_blockDiag

added theorem Continuous.matrix_blockDiagonal'

added theorem Continuous.matrix_blockDiagonal

added theorem Continuous.matrix_col

added theorem Continuous.matrix_conjTranspose

added theorem Continuous.matrix_cramer

added theorem Continuous.matrix_det

added theorem Continuous.matrix_diag

added theorem Continuous.matrix_diagonal

added theorem Continuous.matrix_dotProduct

added theorem Continuous.matrix_elem

added theorem Continuous.matrix_fromBlocks

added theorem Continuous.matrix_map

added theorem Continuous.matrix_mul

added theorem Continuous.matrix_mulVec

added theorem Continuous.matrix_reindex

added theorem Continuous.matrix_row

added theorem Continuous.matrix_submatrix

added theorem Continuous.matrix_trace

added theorem Continuous.matrix_transpose

added theorem Continuous.matrix_updateColumn

added theorem Continuous.matrix_updateRow

added theorem Continuous.matrix_vecMul

added theorem Continuous.matrix_vecMulVec

added theorem HasSum.matrix_blockDiag'

added theorem HasSum.matrix_blockDiag

added theorem HasSum.matrix_blockDiagonal'

added theorem HasSum.matrix_blockDiagonal

added theorem HasSum.matrix_conjTranspose

added theorem HasSum.matrix_diag

added theorem HasSum.matrix_diagonal

added theorem HasSum.matrix_transpose

added theorem Matrix.blockDiagonal'_tsum

added theorem Matrix.blockDiagonal_tsum

added theorem Matrix.conjTranspose_tsum

added theorem Matrix.diagonal_tsum

added theorem Matrix.transpose_tsum

added theorem Summable.matrix_blockDiag'

added theorem Summable.matrix_blockDiag

added theorem Summable.matrix_blockDiagonal'

added theorem Summable.matrix_blockDiagonal

added theorem Summable.matrix_conjTranspose

added theorem Summable.matrix_diag

added theorem Summable.matrix_diagonal

added theorem Summable.matrix_transpose

added theorem continuousAt_matrix_inv

added theorem continuous_matrix

added theorem continuous_matrix_diag

added theorem summable_matrix_blockDiagonal'

added theorem summable_matrix_blockDiagonal

added theorem summable_matrix_conjTranspose

added theorem summable_matrix_diagonal

added theorem summable_matrix_transpose