Theorem HahnSeries.SummableFamily.hsum_unique

Modification history

2025-06-07 08:13
Mathlib/RingTheory/HahnSeries/Summable.lean
feat(HahnSeries): `single_inv` and `single_div_single` (#25414) …
Added HahnSeries.SummableFamily.hsum_uniqueView on Github →