Def HahnSeries.SummableFamily.hsum

Modification history

2024-02-16 04:51

Mathlib/RingTheory/HahnSeries.lean

chore: Split HahnSeries file (#10595) …

Modified HahnSeries.SummableFamily.hsum View on Github →

2023-05-23 12:52

Mathlib/RingTheory/HahnSeries.lean

feat: port RingTheory.HahnSeries (#4261)

Added HahnSeries.SummableFamily.hsum View on Github →