mathlib3

d5a53939 - doc(contribute/index.md): add line about large PRs [ci skip] (#1267)