Commit 2026-08-26 20:09 ee091169

chore(Archive): convert to the module system (#42242) This is just a general good practice these days. Two specific reasons are:

• the module system makes thing faster, for example by reducing how much stuff has to be imported.
• In the long run, we want to only support the module system, and not any non-module system uses of mathlib. #41950 signals this. That way, we can use no_expose, without needing to worry about uses without the module system where the definition will be exposed anyways. The migration is mostly mechanical, akin to what modulize.lean would do: make all imports public, and add @[expose] public section at the beginning of each file. (In a few cases of files without definitions, omit the expose attribute.) Inspired by #36236; re-done by hand. All files omitted there are actually fine to hand-convert.