mathlib

3bd2044b - chore(data/nat/prime): reuse a result from algebra.big_operators.associated (#11143)