Commit 2020-06-26 09:59 5b97da63

View on Github →

feat(ring_theory/matrix_equiv_tensor): matrix n n A ≃ₐ[R] (A ⊗[R] matrix n n R) (#3177) When A is an R-algebra, matrices over A are equivalent (as an algebra) to A ⊗[R] matrix n n R.

Estimated changes

Modified src/algebra/ring.lean

added theorem ring_hom.to_fun_eq_coe

Modified src/data/matrix/basic.lean

added theorem matrix.mul_mul_left

added theorem matrix.mul_mul_right

added def matrix.scalar

added theorem ring_hom.map_matrix_mul

Modified src/linear_algebra/tensor_product.lean

added theorem tensor_product.sum_tmul

added theorem tensor_product.tmul_sum

Modified src/logic/basic.lean

added theorem apply_dite

added theorem apply_ite

added theorem dite_apply

added theorem ite_apply

Modified src/ring_theory/algebra.lean

added theorem alg_equiv.symm_symm

added theorem algebra.algebra_map_eq_smul_one

Created src/ring_theory/matrix_algebra.lean

added theorem algebra_map_matrix_val

added def matrix_equiv_tensor.equiv

added def matrix_equiv_tensor.inv_fun

added theorem matrix_equiv_tensor.inv_fun_add

added theorem matrix_equiv_tensor.inv_fun_algebra_map

added theorem matrix_equiv_tensor.inv_fun_smul

added theorem matrix_equiv_tensor.inv_fun_zero

added theorem matrix_equiv_tensor.left_inv

added theorem matrix_equiv_tensor.right_inv

added def matrix_equiv_tensor.to_fun

added def matrix_equiv_tensor.to_fun_alg_hom

added theorem matrix_equiv_tensor.to_fun_alg_hom_apply

added def matrix_equiv_tensor.to_fun_bilinear

added def matrix_equiv_tensor.to_fun_linear

added def matrix_equiv_tensor.to_fun_right_linear

added def matrix_equiv_tensor

added theorem matrix_equiv_tensor_apply

added theorem matrix_equiv_tensor_apply_symm

Modified src/ring_theory/tensor_product.lean