mathlib
0faa7880 - feat(ring_theory/hahn_series): introduce ring of Hahn series (#6237)

Commit
4 years ago
feat(ring_theory/hahn_series): introduce ring of Hahn series (#6237) Defines Hahn series Provides basic algebraic structure on Hahn series, up to `comm_ring`.
Author
Parents
Loading