mathlib3

feat(src/ring_theory/is_tensor_product): Base change along a surjection.

#17010

Open