[Merged by Bors] - chore: fix implicit-reducible diamond in uniform convergence

[sgouezel]

This one is fixing a diamond which can not be encountered on master, but shows up after the fixes in #38451 (and fixing this diamond is necessary for #38451 to go through).

The diamond is the following. If a space E is a C-module, then it is automatically an R-module (Module.complexToReal). Define now a type synonym E' to E, and declare that, if k acts on E, then it also acts on E', through inferInstanceAs. Then E' is a C-module (instance applied to k=C), and therefore an R-module by Module.complexToReal. But, as E is an R-module (by Module.complexToReal), then E' is also an R-module (by the instance applied to k=R). The two R-module structures are not the same implicit-reducibly, as the latter is hidden behind an opaque function crafted by inferInstanceAs.

To avoid this, we define the smul field by hand instead of hiding it behind an opaque function. This should probably be done throughout Mathlib whenever a type synonym can be endowed with real and complex module structures. I'm just fixing one example here, because it's the one that breaks in #38451.

---

[github-actions]

PR summary def28638ef

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ ofFun

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.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

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