Commit 2021-08-18 10:32 f1b6c8fd

View on Github →

feat(data/matrix/kronecker): add two lemmas (#8700) Added two lemmas kronecker_map_assoc and kronecker_assoc showing associativity of the Kronecker product

Estimated changes

Modified src/data/matrix/kronecker.lean

added theorem matrix.kronecker_assoc

added theorem matrix.kronecker_map_assoc

added theorem matrix.kronecker_map_assoc₁

added def matrix.kronecker_map_bilinear

added theorem matrix.kronecker_map_bilinear_mul_mul

deleted def matrix.kronecker_map_linear

deleted theorem matrix.kronecker_map_linear_mul_mul

added theorem matrix.kronecker_tmul_assoc