mathlib

d6860258 - feat(linear_algebra/pi_tensor_product): add subsingleton_equiv (#10274)

feat(linear_algebra/pi_tensor_product): add subsingleton_equiv (#10274) This is useful for constructing the tensor product of a single module, which we will ultimately need to show an isomorphism to `tensor_algebra`. This also refactors `pempty_equiv` to use `is_empty`, which probably didn't exist at the time. This eliminates a surprising universe variable that was parameterizing `pempty`.