Commit 2025-04-14 07:16 360bf0d2
View on Github →feat (RingTheory/HahnSeries/Multiplication): IsScalarTower and SMulCommClass instances (#24018)
This PR adds instances that show that the scalar multiplication of R on HahnSeries Γ R is compatible with the scalar multiplication of HahnSeries Γ R on HahnModule Γ' R V. Also, module docstrings are updated.