Theorem HahnSeries.SummableFamily.coeff_def

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.coeff_defView on Github →