Commit 2024-07-23 00:55 232c771b

View on Github →

feat (RingTheory/HahnSeries/Multiplication): module structure on HahnModule (#10846) 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.

Estimated changes

Modified Mathlib/Algebra/Order/AddTorsor.lean

Modified Mathlib/Data/Finset/SMulAntidiagonal.lean

deleted theorem Finset.SMulAntidiagonal_min_smul_min

added theorem Finset.smulAntidiagonal_min_smul_min

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

added theorem HahnModule.add_smul

added theorem HahnModule.ext_iff

modified def HahnModule.of

modified theorem HahnModule.of_smul

modified theorem HahnModule.of_symm_smul

added theorem HahnModule.one_smul'

added theorem HahnModule.single_smul_coeff_add

added theorem HahnModule.single_zero_smul_coeff

added theorem HahnModule.single_zero_smul_eq_smul

added theorem HahnModule.smul_add

modified theorem HahnModule.smul_coeff

added theorem HahnModule.smul_coeff_order_add_order

modified theorem HahnModule.smul_coeff_right

added theorem HahnModule.support_smul_subset_vadd_support'

added theorem HahnModule.support_smul_subset_vadd_support

added theorem HahnModule.zero_smul'

added theorem HahnSeries.leadingCoeff_one

Modified Mathlib/RingTheory/HahnSeries/Summable.lean

modified theorem HahnSeries.isUnit_iff