[Merged by Bors] - refactor: generalize SMul (Ideal R) (Submodule R M) to SMul (Submodule R A) (Submodule R M)

[alreadydone]

and redefine Mul (Submodule R A) (Submodule R A) using the latter.

---

• depends on: [Merged by Bors] - perf: speedup using Submodule.restrictScalars_mem instead of relying on defeq #19711

[alreadydone]

!bench

[leanprover-bot]

Here are the benchmark results for commit 6546fad.
There were significant changes against commit 225ff18:

  Benchmark                                  Metric         Change
  ================================================================
- ~Mathlib.Algebra.Algebra.Operations        instructions    20.6%
- ~Mathlib.RingTheory.AdicCompletion.Basic   instructions    12.6%
+ ~Mathlib.RingTheory.Ideal.Cotangent        instructions   -17.6%
+ ~Mathlib.RingTheory.Kaehler.Basic          instructions    -4.9%

[github-actions]

File	Instructions	%
build	+48.904⬝10⁹	(+0.03%)
lint	+4.304⬝10⁹	(+0.06%)
Mathlib.Algebra.Algebra.Operations	+15.912⬝10⁹	(+20.57%)
Mathlib.RingTheory.AdicCompletion.Basic	+10.316⬝10⁹	(+12.57%)
Mathlib.RingTheory.AdicCompletion.Algebra	+9.204⬝10⁹	(+13.59%)

2 files, Instructions +8.0⬝10⁹

File	Instructions	%
Mathlib.RingTheory.Regular.RegularSequence	+8.952⬝10⁹	(+11.12%)
Mathlib.RingTheory.Kaehler.Polynomial	+8.833⬝10⁹	(+6.20%)

File	Instructions	%
Mathlib.RingTheory.AdicCompletion.AsTensorProduct	+7.179⬝10⁹	(+3.67%)
Mathlib.RingTheory.AdicCompletion.Functoriality	+5.215⬝10⁹	(+6.66%)
Mathlib.RingTheory.AdicCompletion.Exactness	+4.39⬝10⁹	(+12.17%)
Mathlib.RingTheory.Filtration	+3.569⬝10⁹	(+9.59%)

3 files, Instructions +2.0⬝10⁹

File	Instructions	%
Mathlib.RingTheory.Ideal.Quotient.Operations	+2.628⬝10⁹	(+2.15%)
Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient	+2.149⬝10⁹	(+13.81%)
Mathlib.RingTheory.LocalRing.Module	+2.33⬝10⁹	(+2.06%)

4 files, Instructions +1.0⬝10⁹

File	Instructions	%
Mathlib.RingTheory.Nakayama	+1.619⬝10⁹	(+14.44%)
Mathlib.LinearAlgebra.TensorProduct.Quotient	+1.497⬝10⁹	(+2.05%)
Mathlib.RingTheory.Kaehler.TensorProduct	+1.138⬝10⁹	(+0.60%)
Mathlib.NumberTheory.RamificationInertia	+1.42⬝10⁹	(+0.47%)

File	Instructions	%
Mathlib.MeasureTheory.Measure.FiniteMeasure	-1.789⬝10⁹	(-2.34%)
Mathlib.RingTheory.Ideal.Operations	-3.599⬝10⁹	(-4.06%)
Mathlib.FieldTheory.RatFunc.Basic	-4.717⬝10⁹	(-2.01%)

2 files, Instructions -18.0⬝10⁹

File	Instructions	%
Mathlib.RingTheory.Kaehler.Basic	-17.499⬝10⁹	(-4.89%)
Mathlib.RingTheory.Ideal.Cotangent	-17.733⬝10⁹	(-17.58%)

[riccardobrasca]

Can you please merge master and bench again?

[alreadydone]

!bench

[leanprover-bot]

Here are the benchmark results for commit d81cc44.
There were significant changes against commit a893180:

  Benchmark                             Metric         Change
  ===========================================================
- ~Mathlib.Algebra.Algebra.Operations   instructions    15.7%
+ ~Mathlib.RingTheory.Ideal.Cotangent   instructions   -18.2%
+ ~Mathlib.RingTheory.Kaehler.Basic     instructions    -5.3%

[alreadydone]

Hmm, looks like a rather positive change! Mathlib.Algebra.Algebra.Operations got 15.7% slower but also 12.2% longer.

[leanprover-bot]

Here are the benchmark results for commit d3c5b98.
There were significant changes against commit a893180:

  Benchmark                             Metric         Change
  ===========================================================
- ~Mathlib.Algebra.Algebra.Operations   instructions    15.7%
+ ~Mathlib.RingTheory.Ideal.Cotangent   instructions   -18.2%
+ ~Mathlib.RingTheory.Kaehler.Basic     instructions    -5.3%

[alreadydone]

Hmm, looks like a rather positive change! Mathlib.Algebra.Algebra.Operations got 15.7% slower but also 12.2% longer.

Sorry, false alarm. The sped-up files were changed to avoid timeouts. Let me single those out to a separate PR ...

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - perf: speedup using Submodule.restrictScalars_mem instead of relying on defeq #19711
  By Dependent Issues (🤖). Happy coding!

[alreadydone]

!bench

[leanprover-bot]

Here are the benchmark results for commit efe2593.
There were significant changes against commit d7abea9:

  Benchmark                             Metric         Change
  ===========================================================
- ~Mathlib.Algebra.Algebra.Operations   instructions    15.7%

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style