mathlib3

4daaff06 - feat(data/nat/prime): factors sublist of product (#11104)

feat(data/nat/prime): factors sublist of product (#11104) This PR changes the existing `factors_subset_right` to give a stronger sublist conclusion (which trivially can be used to reproduce the subst version).