Commit 2024-07-13 18:48 100eb1d0

View on Github →

feat (RingTheory/HahnSeries) SMulZeroClass instances (#13421) This PR adds instances for SMulZeroClass R (HahnSeries Γ R) and SMulZeroClass R (HahnModule Γ R V). Also, some minor variable cleanup.

Estimated changes

Modified Mathlib/RingTheory/HahnSeries/Addition.lean

added theorem HahnSeries.orderTop_smul_not_lt

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

modified def HahnModule.of

added theorem HahnModule.of_smul

added theorem HahnModule.of_symm_smul

modified theorem HahnModule.smul_coeff_left

modified theorem HahnModule.smul_coeff_right