Def HahnSeries.SummableFamily.single

Modification history

2025-06-07 08:13

Mathlib/RingTheory/HahnSeries/Summable.lean

feat(HahnSeries): `single_inv` and `single_div_single` (#25414) …

Modified HahnSeries.SummableFamily.single View on Github →

2024-10-18 17:35

Mathlib/RingTheory/HahnSeries/Summable.lean

feat (RingTheory/HahnSeries/Summable) : singleton summable family (#16871) …

Added HahnSeries.SummableFamily.single View on Github →