[Merged by Bors] - chore: remove import alls by making some norm_num components public - #42457

[Merged by Bors] - chore: remove import alls by making some norm_num components public#42457

thorimur wants to merge 8 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

thorimur:chore-factors-import-allthorimur/mathlib4:chore-factors-import-allCopy head branch name to clipboard