Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-06-05 02:20 30882647

View on Github →

chore(archive/imo): fix some naming inconsistencies and whitespace (#19155) I realize that this is the third PR concerning namespacing the files in archive/imo. These are some simple inconsistencies in naming. There is no rush in merging this PR, but in the long run it might help to have consistent namespacing, so that batch renames can be simpler.

Estimated changes