Theorem HahnSeries.addVal_apply_of_ne
Modification history
2024-07-16 22:44
Mathlib/RingTheory/HahnSeries/Summable.lean
chore: (RingTheory/HahnSeries) : Move valuation material to new file (#14807) …
Modified HahnSeries.addVal_apply_of_neView on Github →