Commit 2023-05-17 23:10 56773eb8

View on Github →

feat: port RingTheory.TensorProduct (#4004)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/TensorProduct.lean

added theorem Algebra.TensorProduct.adjoin_tmul_eq_top

added def Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct

added theorem Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct_apply

added def Algebra.TensorProduct.algEquivOfLinearEquivTripleTensorProduct

added theorem Algebra.TensorProduct.algEquivOfLinearEquivTripleTensorProduct_apply

added def Algebra.TensorProduct.algHomOfLinearMapTensorProduct

added theorem Algebra.TensorProduct.algHomOfLinearMapTensorProduct_apply

added theorem Algebra.TensorProduct.algebraMap_apply

added theorem Algebra.TensorProduct.assoc_aux_1

added theorem Algebra.TensorProduct.assoc_aux_2

added theorem Algebra.TensorProduct.assoc_tmul

added theorem Algebra.TensorProduct.basisAux_map_smul

added theorem Algebra.TensorProduct.basisAux_tmul

added theorem Algebra.TensorProduct.basis_repr_symm_apply'

added theorem Algebra.TensorProduct.basis_repr_symm_apply

added theorem Algebra.TensorProduct.basis_repr_tmul

added theorem Algebra.TensorProduct.comm_tmul

added def Algebra.TensorProduct.congr

added theorem Algebra.TensorProduct.congr_apply

added theorem Algebra.TensorProduct.congr_symm_apply

added theorem Algebra.TensorProduct.ext

added def Algebra.TensorProduct.includeLeft

added def Algebra.TensorProduct.includeLeftRingHom

added theorem Algebra.TensorProduct.includeLeft_apply

added theorem Algebra.TensorProduct.includeLeft_comp_algebraMap

added def Algebra.TensorProduct.includeRight

added theorem Algebra.TensorProduct.includeRight_apply

added theorem Algebra.TensorProduct.lid_tmul

added def Algebra.TensorProduct.lmul'

added theorem Algebra.TensorProduct.lmul'_apply_tmul

added theorem Algebra.TensorProduct.lmul'_comp_includeLeft

added theorem Algebra.TensorProduct.lmul'_comp_includeRight

added theorem Algebra.TensorProduct.lmul'_toLinearMap

added def Algebra.TensorProduct.map

added theorem Algebra.TensorProduct.map_comp_includeLeft

added theorem Algebra.TensorProduct.map_comp_includeRight

added theorem Algebra.TensorProduct.map_range

added theorem Algebra.TensorProduct.map_tmul

added def Algebra.TensorProduct.mul

added def Algebra.TensorProduct.mulAux

added theorem Algebra.TensorProduct.mulAux_apply

added theorem Algebra.TensorProduct.mul_apply

added theorem Algebra.TensorProduct.mul_assoc'

added theorem Algebra.TensorProduct.mul_one

added theorem Algebra.TensorProduct.one_def

added theorem Algebra.TensorProduct.one_mul

added def Algebra.TensorProduct.productLeftAlgHom

added def Algebra.TensorProduct.productMap

added theorem Algebra.TensorProduct.productMap_apply_tmul

added theorem Algebra.TensorProduct.productMap_left

added theorem Algebra.TensorProduct.productMap_left_apply

added theorem Algebra.TensorProduct.productMap_range

added theorem Algebra.TensorProduct.productMap_right

added theorem Algebra.TensorProduct.productMap_right_apply

added theorem Algebra.TensorProduct.rid_tmul

added def Algebra.TensorProduct.rightAlgebra

added theorem Algebra.TensorProduct.tmul_mul_tmul

added theorem Algebra.TensorProduct.tmul_pow

added def LinearMap.baseChange

added def LinearMap.baseChangeHom

added theorem LinearMap.baseChange_add

added theorem LinearMap.baseChange_eq_ltensor

added theorem LinearMap.baseChange_neg

added theorem LinearMap.baseChange_smul

added theorem LinearMap.baseChange_sub

added theorem LinearMap.baseChange_tmul

added theorem LinearMap.baseChange_zero

added def Module.endTensorEndAlgHom

added theorem Module.endTensorEndAlgHom_apply

added theorem Subalgebra.finiteDimensional_sup

added def TensorProduct.Algebra.moduleAux

added theorem TensorProduct.Algebra.moduleAux_apply

added theorem TensorProduct.Algebra.smul_def

added def TensorProduct.AlgebraTensorModule.assoc

added theorem TensorProduct.AlgebraTensorModule.ext

added def TensorProduct.AlgebraTensorModule.lcurry

added def TensorProduct.AlgebraTensorModule.lift.equiv

added theorem TensorProduct.AlgebraTensorModule.lift_apply

added theorem TensorProduct.AlgebraTensorModule.lift_tmul

added theorem TensorProduct.AlgebraTensorModule.restrictScalars_curry

added theorem TensorProduct.AlgebraTensorModule.smul_eq_lsmul_rtensor

added def TensorProduct.AlgebraTensorModule.uncurry