[Merged by Bors] - chore(Mathlib/Tactic): stop norm_num importing the Bochner integral#39602

b-mehta wants to merge 9 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

b-mehta:norm-num-bochnerb-mehta/mathlib4:norm-num-bochnerCopy head branch name to clipboard