Commit 2026-09-08 22:52 56124ab7

chore: remove imports added by shake (#40961) This PR removes some imports that were added by shake in the past. For some of these it's not clear to me why shake added them. In particular, I noticed some occurrences of public import Mathlib.Tactic.NormNum.Pow/Inv, where norm_num is not used in the file at all, which I found suspicious. For CompileInductive, it is expected that shake keeps the import, because of shake: keep-downstream, so these imports need to be minimzed manually, which this PR does. For good measure, I also fixed an issue in Mathlib.Tactic.NormNum.Pow that some non-meta things were marked as meta.