Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-07 11:06 6c8203f2

View on Github →

chore(linear_algebra/bilinear_map): split off new file from linear_algebra/tensor_product (#9054) The first part of linear_algebra/tensor_product consisted of some basics on bilinear maps that are not directly related to the construction of the tensor product. This PR moves them to a new file.

Estimated changes

added theorem linear_map.ext₂
added def linear_map.flip
added theorem linear_map.flip_apply
added theorem linear_map.flip_inj
added theorem linear_map.ker_lsmul
added def linear_map.lcomp
added theorem linear_map.lcomp_apply
added def linear_map.lflip
added theorem linear_map.lflip_apply
added def linear_map.lsmul
added theorem linear_map.lsmul_apply
added theorem linear_map.map_add₂
added theorem linear_map.map_neg₂
added theorem linear_map.map_smul₂
added theorem linear_map.map_sub₂
added theorem linear_map.map_sum₂
added theorem linear_map.map_zero₂
added def linear_map.mk₂
added theorem linear_map.mk₂_apply
deleted def linear_map.compl₂
deleted theorem linear_map.compl₂_apply
deleted def linear_map.compr₂
deleted theorem linear_map.compr₂_apply
deleted theorem linear_map.ext₂
deleted def linear_map.flip
deleted theorem linear_map.flip_apply
deleted theorem linear_map.flip_inj
deleted theorem linear_map.ker_lsmul
deleted def linear_map.lcomp
deleted theorem linear_map.lcomp_apply
deleted def linear_map.lflip
deleted theorem linear_map.lflip_apply
deleted def linear_map.llcomp
deleted theorem linear_map.llcomp_apply
deleted def linear_map.lsmul
deleted theorem linear_map.lsmul_apply
deleted theorem linear_map.map_add₂
deleted theorem linear_map.map_neg₂
deleted theorem linear_map.map_smul₂
deleted theorem linear_map.map_sub₂
deleted theorem linear_map.map_sum₂
deleted theorem linear_map.map_zero₂
deleted def linear_map.mk₂'
deleted theorem linear_map.mk₂'_apply
deleted def linear_map.mk₂
deleted theorem linear_map.mk₂_apply