Theorem HahnModule.of_sub

Modification history

2025-10-11 16:33

Mathlib/RingTheory/HahnSeries/Multiplication.lean

feat (RingTheory/HahnSeries/Multiplication): Add group instances to HahnModule (#29772) …

Added HahnModule.of_sub View on Github →