Def HahnSeries.to_iterate

Modification history

2024-05-17 08:20
Mathlib/RingTheory/HahnSeries/Basic.lean
feat: HahnSeries on Lex product (#10781) …
Deleted HahnSeries.to_iterateView on Github →
2024-02-16 04:51
Mathlib/RingTheory/HahnSeries/Basic.lean
chore: Split HahnSeries file (#10595) …
Added HahnSeries.to_iterateView on Github →