Commit 2021-02-26 13:13 20b49fbd

View on Github →

feat(linear_algebra/tensor_product): allow different semirings in linear_map.flip (#6414) This also means the map_*₂ lemmas are more generally applicable to linear_maps over different rings, such as linear_map.prod_equiv.to_linear_map. To avoid breakage, this leaves mk₂ R for when R is commutative, and introduces mk₂' R S for when two different rings are wanted.

Estimated changes

Modified src/linear_algebra/tensor_product.lean

modified theorem linear_map.ext₂

modified def linear_map.flip

modified theorem linear_map.flip_apply

modified theorem linear_map.flip_inj

modified def linear_map.lflip

modified theorem linear_map.map_add₂

modified theorem linear_map.map_neg₂

modified theorem linear_map.map_smul₂

modified theorem linear_map.map_sub₂

modified theorem linear_map.map_zero₂

added def linear_map.mk₂'

added theorem linear_map.mk₂'_apply