[Merged by Bors] - perf(Analysis/RCLike/Basic): move a section#38034

kbuzzard wants to merge 2 commits intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

kbuzzard:kbuzzard-move-norm-lemmaskbuzzard/mathlib4:kbuzzard-move-norm-lemmasCopy head branch name to clipboard