mathlib

10b4e499 - chore(data/nat/prime): reduce imports more (#17854)

chore(data/nat/prime): reduce imports more (#17854) This relocates the `norm_num` plugin and `nat.factors`, and rewrites a proof without `wlog`, to avoid depending on a reasonably sized chunk of results about `list`s.