Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-13 01:22 a945b187

View on Github →

feat(linear_algebra/tensor_product): tensor_product.map is bilinear in its two arguments (#13608)

Estimated changes

Modified src/linear_algebra/dual.lean

added def tensor_product.dual_distrib

added theorem tensor_product.dual_distrib_apply

added def tensor_product.dual_distrib_equiv

added def tensor_product.dual_distrib_inv_of_basis

added theorem tensor_product.dual_distrib_inv_of_basis_apply

Modified src/linear_algebra/tensor_product.lean

added def tensor_product.hom_tensor_hom_map

added theorem tensor_product.hom_tensor_hom_map_apply

added theorem tensor_product.map_add_left

added theorem tensor_product.map_add_right

added def tensor_product.map_bilinear

added theorem tensor_product.map_bilinear_apply

added theorem tensor_product.map_smul_left

added theorem tensor_product.map_smul_right

added theorem tensor_product.smul_tmul_smul

Modified src/ring_theory/tensor_product.lean

added def module.End_tensor_End_alg_hom

added theorem module.End_tensor_End_alg_hom_apply