[Merged by Bors] - chore: reduce imports in ZMod.Basic

[Ruben-VandeVelde]

• While at it, document the lemmas that were moved, and two similar lemmas in ZMod.Basic.

---

• The extra import Mathlib.RingTheory.ZMod import in Mathlib/Data/ZMod/Quotient.lean and Mathlib/NumberTheory/Padics/RingHoms.lean is probably not too bad (shake didn't speak yet, so perhaps that is even superfluous).

[grunweg]

Commenting to avoid duplicate work: I'm trying to pick this up.

[grunweg]

This is almost ready: there is one build error to fix in Data/Zmod/Quotient.

[grunweg]

@Ruben-VandeVelde I'd declare this done (modulo further build errors, but I cannot imagine those). Feel free to take a look.

[Ruben-VandeVelde]

The parts I didn't do look good :)

[grunweg]

I think this can be removed, #12487 confirms this.

Suggested change

import Mathlib.Tactic.FinCases

[Ruben-VandeVelde]

Presumably because it's imported transitively, because this file does use fin_cases

[Vierkantor]

I also complained about the fact that shake doesn't warn about transitive imports, but apparently that's supposed to be a feature. So I'll let you decide whether it's best to keep or remove.

Looks good to me otherwise, thanks!

bors d+

[mathlib-bors]

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

[Ruben-VandeVelde]

bors merge

[mathlib-bors]

Build failed:

• Build

[grunweg]

@Ruben-VandeVelde This builds again :-)

[Ruben-VandeVelde]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style