mathlib3

601ea914 - feat(data/nat/mul_ind): generalise rec_on_prime to assume positivity (#11714)

feat(data/nat/mul_ind): generalise rec_on_prime to assume positivity (#11714) This makes the multiplicative induction principles slightly stronger, as the coprimality part can assume the given values are positive.