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

[kbuzzard]

These lemmas compile more quickly if RCLike ℝ is available, so move them lower in the file.

---

Random fact: changing the definition of Ring R from extends Semiring R, AddCommGroup R, AddGroupWithOne R to extends Semiring R, AddCommGroupWithOne R causes very little breakage in mathlib, but one thing it does break is the proof of RCLike.norm_expect_le. Intrigued, I investigated further. What's happening is that the lemmas in the section which this PR moves need HSMul ℚ≥0 ℝ ℝ or Module ℚ≥0 ℝ which they all want to get from RCLike ℝ but typeclass inference goes on a wild goose chase for this instance because it is only defined later in the file! Fiddling with the algebra hierarchy (which I'm currently doing) makes the wild goose chase slightly longer and triggers a timeout.

However moving the section to just after the definition of RCLike ℝ makes two of the three lemmas compile more quickly: RCLike.norm_nnqsmul goes from 728878 mHeartbeats to 220634 and RCLike.norm_expect_le goes from 1308705 to 802785 (the third is unchanged). Rather than doing the moving as part of the algebra refactor PR I thought I'd just split it off as it seemed uncontroversial.

[github-actions]

PR summary 00dbc4ec64

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[grunweg]

!bench

[leanprover-radar]

Benchmark results for 5a3bcef against 00dbc4e are in. No significant results found. @grunweg

• ✅ build//instructions: -12.2G (-0.01%)

Small changes (1✅)

• ✅ build/module/Mathlib.Analysis.RCLike.Basic//instructions: -3.2G (-3.22%)

[grunweg]

The diff looks straightforward; do you think a comment about their location being deliberate is worth it?

Otherwise, LGTM assuming benchmarks are good; thanks for doing this!

[grunweg]

Thanks!
bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-Build Step
• ci (staging) / Lint style
• ci (staging) / Build
• ci (staging) / Post-CI job