Mathlib Changelog
v4
Changelog
About
Github
Theorem
HahnSeries.SummableFamily.hsum_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.hsum_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.hsum_single
View on Github →