[Merged by Bors] - docs(data/pnat): add module docstrings

[YaelDillies]

---

I don't like those two files, xgcd in particular, for several reasons:

For xgcd,

• xgcd_type is literally ℕ × ℕ × ℕ × ℕ × ℕ × ℕ with custom fields names. At least is_special could be bundled with it.
• It basically is nat.xgcd (which already existed at the time of Neil Strickland's commit, feat (data/pnat): extensions to pnat  #1073) but with no mention to ℤ.
• Instead of proving an equivalence between a definition and another condition, it defines this other condition separately and then proves its equivalence with the original one (see is_special/is_special', is_reduced/is_reduced'), and this isn't justified by defeq concerns or similar.
• It outsources all steps out of the algorithm while it's not very long and none of these steps is truly useful beyond that scope. This results in multiple lemmas being sexplicated.

For factors,

• Most of the file is rederiving instances by hand, from the fact that prime_multiset is a subtype.
• It is not general enough.

Neither file is ever imported, which suggests that they are currently of limited use.

Any opinion?

[jcommelin]

Thanks. I have one comment about the module docstring. If you agree, please merge the suggestion and kick this on the queue.

bors d+

(Sorry for being so late with the review.)

[bors]

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[YaelDillies]

bors merge

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests