mathlib3

7b641cba - chore(number_theory/primorial): golf some proofs (#11024)