Commit 2023-05-18 08:40 968d650c

View on Github →

feat: port Data.Matrix.Kronecker (#4068)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Matrix/Kronecker.lean

added theorem Matrix.add_kronecker

added theorem Matrix.add_kroneckerTMul

added theorem Matrix.det_kronecker

added theorem Matrix.det_kroneckerMapBilinear

added theorem Matrix.det_kroneckerTMul

added theorem Matrix.diagonal_kronecker

added theorem Matrix.diagonal_kroneckerTMul

added theorem Matrix.diagonal_kroneckerTMul_diagonal

added theorem Matrix.diagonal_kronecker_diagonal

added theorem Matrix.inv_kronecker

added def Matrix.kronecker

added def Matrix.kroneckerBilinear

added def Matrix.kroneckerMap

added def Matrix.kroneckerMapBilinear

added theorem Matrix.kroneckerMapBilinear_mul_mul

added theorem Matrix.kroneckerMap_add_left

added theorem Matrix.kroneckerMap_add_right

added theorem Matrix.kroneckerMap_apply

added theorem Matrix.kroneckerMap_assoc

added theorem Matrix.kroneckerMap_assoc₁

added theorem Matrix.kroneckerMap_diagonal_diagonal

added theorem Matrix.kroneckerMap_diagonal_left

added theorem Matrix.kroneckerMap_diagonal_right

added theorem Matrix.kroneckerMap_map

added theorem Matrix.kroneckerMap_map_left

added theorem Matrix.kroneckerMap_map_right

added theorem Matrix.kroneckerMap_one_one

added theorem Matrix.kroneckerMap_reindex

added theorem Matrix.kroneckerMap_reindex_left

added theorem Matrix.kroneckerMap_reindex_right

added theorem Matrix.kroneckerMap_smul_left

added theorem Matrix.kroneckerMap_smul_right

added theorem Matrix.kroneckerMap_transpose

added theorem Matrix.kroneckerMap_zero_left

added theorem Matrix.kroneckerMap_zero_right

added def Matrix.kroneckerTMul

added def Matrix.kroneckerTMulBilinear

added theorem Matrix.kroneckerTMul_add

added theorem Matrix.kroneckerTMul_apply

added theorem Matrix.kroneckerTMul_assoc'

added theorem Matrix.kroneckerTMul_assoc

added theorem Matrix.kroneckerTMul_diagonal

added theorem Matrix.kroneckerTMul_smul

added theorem Matrix.kroneckerTMul_zero

added theorem Matrix.kronecker_add

added theorem Matrix.kronecker_apply

added theorem Matrix.kronecker_assoc'

added theorem Matrix.kronecker_assoc

added theorem Matrix.kronecker_diagonal

added theorem Matrix.kronecker_one

added theorem Matrix.kronecker_smul

added theorem Matrix.kronecker_zero

added theorem Matrix.mul_kroneckerTMul_mul

added theorem Matrix.mul_kronecker_mul

added theorem Matrix.one_kronecker

added theorem Matrix.one_kroneckerTMul_one

added theorem Matrix.one_kronecker_one

added theorem Matrix.smul_kronecker

added theorem Matrix.smul_kroneckerTMul

added theorem Matrix.trace_kronecker

added theorem Matrix.trace_kroneckerMapBilinear

added theorem Matrix.trace_kroneckerTMul

added theorem Matrix.zero_kronecker

added theorem Matrix.zero_kroneckerTMul