mathlib3

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

#1267

Merged