[Merged by Bors] - feat(ring_theory/tensor_product): A predicate for being the tensor product.

[erdOne]

---

[eric-wieser]

Would it make sense to follow the design of direct_sum.decomposition here and provide an explicit inverse?

[erdOne]

I would prefer if this is a Prop and does not contain any data. Besides, the inverse of this is usually not that constructive, for example the inverse M_p -> A_p x M takes a choice of fraction m/s to 1/s x m, but there isn't a canonical choice of the fraction representation.

[eric-wieser]

I don't really understand your comment about canonicity; the inverse is always canonical because it's unique, right?

My thinking behind making the typeclass carry data is that an instance can still always provide it non-computably; but we don't have to throw away computability to use tensor_product through this API.

[erdOne]

I thought the main concern were bad defeqs, and what I was saying that the definition of the inverse is usually no better than "the inverse of the lift".
But still I don't think there are many cases where there is a computable inverse? Maybe M/IM -> A/I x M since quotients seem to be computable?
I think the choice I made is in line with the approach we took on localizations: we have a computable localization and an Prop-valued is_localization whose API are mostly incomputable.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests