mathlib

ba9c8f35 - feat(ring_theory/tensor_product): A predicate for being the tensor product. (#15512)