[Merged by Bors] - chore(archive/imo): change namespace `imo` to `imoYYYY_qX`

[adomani]

This PR fixes a mistake that I made when namespacing files in archive.imo. Now, the files whose namespace was imo have namespace their file name (minus .lean).

Changes:

• namespace imo changed to imoYYYY_qX;
• added nolint dup_namespace tags to the declarations that have a duplication;
• changed namespace imo_1987_q1 to imo1987_q1 for consistency.

Zulip discussion

---

[eric-wieser]

You'll probably want to open imo_XXXX_q4 immediately after end imo_XXXX_q4

[semorrison]

bors p=10

[semorrison]

bors merge

[bors[bot]]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here. For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

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