Def HahnSeries.SummableFamily.coeff

Modification history

2024-10-22 21:35
Mathlib/RingTheory/HahnSeries/Summable.lean
feat (RingTheory/HahnSeries/Summable) : coeff function for a summable family (#16649) …
Added HahnSeries.SummableFamily.coeffView on Github →