Commit 2025-10-11 16:33 7950cd56

View on Github →

feat (RingTheory/HahnSeries/Multiplication): Add group instances to HahnModule (#29772) This PR adds Zero and AddCommGroup instances to HahnModule when appropriate. We also add comparison lemmas for subtraction in the AddCommGroup case, and reorganize some variables.

Estimated changes

modified theorem HahnModule.coeff_smul
modified theorem HahnModule.of_add
added theorem HahnModule.of_sub
modified theorem HahnModule.of_symm_add
added theorem HahnModule.of_symm_sub
modified theorem HahnModule.of_symm_zero
modified theorem HahnModule.of_zero