mathlib3

dc48a849 - feat(linear_algebra/pi_tensor_product): add reindex and pempty_equiv (#6069)