mathlib3

30882647 - chore(archive/imo): fix some naming inconsistencies and whitespace (#19155)

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.