Theorem HahnSeries.SummableFamily.powers_of_not_orderTop_pos

Modification history

2025-06-07 08:13

Mathlib/RingTheory/HahnSeries/Summable.lean

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

Modified HahnSeries.SummableFamily.powers_of_not_orderTop_pos View on Github →

2025-05-09 18:56

Mathlib/RingTheory/HahnSeries/Summable.lean

chore (RingTheory/HahnSeries/SummableFamily): refactor HahnSeries.SummableFamily.powers to take junk values (#22959) …

Added HahnSeries.SummableFamily.powers_of_not_orderTop_pos View on Github →