Theorem HahnSeries.one_sub_single_neg_mul

Modification history

2026-10-06 22:43
Mathlib/RingTheory/HahnSeries/Summable.lean
chore: deprecate `plus` and `minus` in names (#44566) …
Added HahnSeries.one_sub_single_neg_mulView on Github →