Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-03 11:07 ef139383

View on Github →

feat(ring_theory/tensor_product): the base change of a linear map along an algebra (#4773)

Estimated changes

Modified src/algebra/lie/weights.lean

Modified src/linear_algebra/tensor_product.lean

added theorem linear_map.ltensor_mul

added theorem linear_map.rtensor_mul

added theorem tensor_product.curry_injective

modified theorem tensor_product.smul_tmul'

modified theorem tensor_product.smul_tmul

modified theorem tensor_product.tmul_smul

Modified src/ring_theory/tensor_product.lean

added def linear_map.base_change

added theorem linear_map.base_change_add

added theorem linear_map.base_change_eq_ltensor

added def linear_map.base_change_hom

added theorem linear_map.base_change_neg

added theorem linear_map.base_change_smul

added theorem linear_map.base_change_sub

added theorem linear_map.base_change_tmul

added theorem linear_map.base_change_zero

added def tensor_product.algebra_tensor_module.assoc

added def tensor_product.algebra_tensor_module.curry

added theorem tensor_product.algebra_tensor_module.curry_injective

added theorem tensor_product.algebra_tensor_module.ext

added def tensor_product.algebra_tensor_module.lcurry

added def tensor_product.algebra_tensor_module.lift.equiv

added def tensor_product.algebra_tensor_module.lift

added theorem tensor_product.algebra_tensor_module.lift_tmul

added def tensor_product.algebra_tensor_module.mk

added theorem tensor_product.algebra_tensor_module.restrict_scalars_curry

added theorem tensor_product.algebra_tensor_module.smul_eq_lsmul_rtensor

added def tensor_product.algebra_tensor_module.uncurry