Commit 2021-09-07 05:56 5b29630d

chore(linear_algebra/tensor_product): remove @[ext] tag from tensor_product.mk_compr₂_inj (#8868) This PR removes the @[ext] tag from tensor_product.mk_compr₂_inj and readds it locally only where it is needed. This is a workaround for the issue discussed in this Zulip thread: basically, when ext tries to apply this lemma to linear maps, it fails only after a very long typeclass search. While this problem is already present to some extent in current mathlib, it is exacerbated by the upcoming generalization of linear maps to semilinear maps. In addition to this change, a few individual uses of ext have been replaced by a manual application of the relevant ext lemma(s) for performance reasons. For discoverability, the lemma tensor_product.mk_compr₂_inj is renamed to tensor_product.ext and the former tensor_product.ext to tensor_product.ext'.