mathlib

e221dc9a - feat(ring_theory/hahn_series): algebra structure, equivalences with power series (#6540)

feat(ring_theory/hahn_series): algebra structure, equivalences with power series (#6540) Places an `algebra` structure on `hahn_series` Defines a `ring_equiv` and when relevant an `alg_equiv` between `hahn_series nat R` and `power_series R`. Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>