mathlib3
5f25c089 - chore(archive/imo): change namespace `imo` to `imoYYYY_qX` (#19152)

Commit
2 years ago
chore(archive/imo): change namespace `imo` to `imoYYYY_qX` (#19152) 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](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/mathport/near/363379951) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading