feat (RingTheory/HahnSeries/Multiplication): module structure on HahnModule

[ScottCarnahan]

trafficstars

We add some theorems and instances for Hahn Modules, in particular, a HahnSeries Γ R-module structure on HahnModule Γ R V for R a semiring and V an R-module. Some HahnSeries Mul results are reduced to the corresponding SMul results.

---

• [ ] depends on: #11979 [OrderedVAdd]
• [ ] depends on: #12996 [leadingCoeff]

[ScottCarnahan]

@alreadydone suggested marking the definition of of reducible. I tried it, and it had the following effects:

1. all @[simp] lemmas with of in the statement made the simpNF linter angry - it wanted me to switch to Equiv.refl.
2. some proofs using simp broke, and as I was fixing them, I felt like simp was pushing me away from the goals every time I tried to use it.

Is there some way to fix this behavior?

[github-actions[bot]]

Import summary

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.HahnSeries.Multiplication	885	887	+2 (+0.23%)
Mathlib.RingTheory.HahnSeries.Summable	895	897	+2 (+0.22%)

[github-actions[bot]]

PR summary 5f84931803

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.HahnSeries.Multiplication	923	926	+3 (+0.33%)
Mathlib.RingTheory.HahnSeries.Summable	926	929	+3 (+0.32%)

Import changes for all files

Files	Import difference
6 files Mathlib.RingTheory.LaurentSeries Mathlib.Algebra.Vertex.HVertexOperator Mathlib.RingTheory.HahnSeries.Valuation Mathlib.RingTheory.HahnSeries.Summable Mathlib.RingTheory.HahnSeries.PowerSeries Mathlib.RingTheory.HahnSeries.Multiplication	3

---

Declarations diff

+ add_smul + ext_iff + instDistribSMul + instModule + instNoZeroSMulDivisors + leadingCoeff_one + one_smul' + single_smul_coeff_add + single_zero_smul_coeff + single_zero_smul_eq_smul + smulAntidiagonal_min_smul_min + smul_add + smul_coeff_order_add_order + support_smul_subset_vadd_support + support_smul_subset_vadd_support' + zero_smul' - SMulAntidiagonal_min_smul_min

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>

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#11979~~
• ~~leanprover-community/mathlib4#12996~~
• ~~leanprover-community/mathlib4#13421~~
• ~~leanprover-community/mathlib4#14479~~ By Dependent Issues (🤖). Happy coding!

[jcommelin]

I spotted a typo just outside your diff. If you don't mind, please fix it as part of this PR.

Otherwise, LGTM

bors d+

[mathlib-bors[bot]]

:v: ScottCarnahan can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[ScottCarnahan]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style