mathlib3

20b49fbd - feat(linear_algebra/tensor_product): allow different semirings in linear_map.flip (#6414)

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.