feat(Topology/Algebra/Field): ContinuousSMul for intermediate fields

[jjdishere]

If M is an intermediate field between field extension L/K, then M acts continuously on L and bot act continuously on M. The M acts continuously on L part is proved in a more general setup.

---

• depends on: [Merged by Bors] - feat(FieldTheory): define induced action of subfields and intermediate fields #18141
  

[github-actions]

PR summary f47c38cd66

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Topology.Algebra.IntermediateField	1382

---

Declarations diff

+ IntermediateField.botContinuousSMul
+ IntermediateField.continuousSMul
+ Subalgebra.continuousSMul
+ Subfield.continuousSMul
+ Subring.continuousSMul
+ continuousSMul

You can run this locally as follows

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

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

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

[jjdishere]

The large import change is caused by the bot element of IntermediateField being defined unexpectedly late. It could be defined as early as in the file containing IntermediateField's definition. However, it is not defined until the file Mathlib.FieldTheory.Adjoin.

In order to solve this, I created a new file specialized for the ContinuousSMul instances for intermediate fields.

[jjdishere]

!bench

[leanprover-bot]

Here are the benchmark results for commit 774ee5e.
The entire run failed.
Found no significant differences.

[jjdishere]

!bench

[leanprover-bot]

Here are the benchmark results for commit b0efef1.
There were significant changes against commit e98856a:

  Benchmark                                          Metric         Change
  ========================================================================
- ~Mathlib.FieldTheory.Galois.Profinite              instructions    30.9%
+ ~Mathlib.FieldTheory.IntermediateField.Algebraic   instructions   -22.7%
- ~Mathlib.FieldTheory.IntermediateField.Basic       instructions     8.8%
+ ~Mathlib.NumberTheory.NumberField.Discriminant     instructions    -7.9%

[github-actions]

File	Instructions	%
build	-560.257⬝10⁹	(+0.42%)
lint	-103.439⬝10⁹	(+1.57%)
Mathlib.FieldTheory.Galois.Profinite	+14.239⬝10⁹	(+30.85%)
Mathlib.FieldTheory.IntermediateField.Basic	+10.692⬝10⁹	(+8.80%)

2 files, Instructions +4.0⬝10⁹

File	Instructions	%
Mathlib.Algebra.Field.Subfield	+4.200⬝10⁹	(+7.24%)
Mathlib.RepresentationTheory.GroupCohomology.Resolution	+4.103⬝10⁹	(+2.81%)

4 files, Instructions +1.0⬝10⁹

File	Instructions	%
Mathlib.FieldTheory.SeparableDegree	+1.914⬝10⁹	(+1.20%)
Mathlib.FieldTheory.Fixed	+1.441⬝10⁹	(+1.48%)
Mathlib.FieldTheory.PrimitiveElement	+1.301⬝10⁹	(+2.29%)
Mathlib.Topology.Algebra.Ring.Basic	+1.24⬝10⁹	(+7.74%)

2 files, Instructions -2.0⬝10⁹

File	Instructions	%
Mathlib.FieldTheory.PurelyInseparable	-1.24⬝10⁹	(+0.50%)
Mathlib.FieldTheory.PolynomialGaloisGroup	-1.646⬝10⁹	(+3.77%)

2 files, Instructions -4.0⬝10⁹

File	Instructions	%
Mathlib.RingTheory.Trace.Basic	-3.153⬝10⁹	(+3.73%)
Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots	-3.974⬝10⁹	(+5.52%)

File	Instructions	%
Mathlib.RingTheory.Norm.Basic	-4.456⬝10⁹	(+7.56%)

2 files, Instructions -6.0⬝10⁹

File	Instructions	%
Mathlib.FieldTheory.SeparableClosure	-5.254⬝10⁹	(+8.8%)
Mathlib.FieldTheory.Galois.Basic	-5.917⬝10⁹	(+6.95%)

File	Instructions	%
Mathlib.FieldTheory.Adjoin	-6.71⬝10⁹	(+2.20%)
Mathlib.FieldTheory.IntermediateField.Algebraic	-11.941⬝10⁹	(+22.68%)
Mathlib.NumberTheory.NumberField.Discriminant	-17.290⬝10⁹	(+7.94%)

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(FieldTheory): define induced action of subfields and intermediate fields #18141
  By Dependent Issues (🤖). Happy coding!