Commit 2024-06-24 10:09 6f8b1536

View on Github →

fix: generalize HahnSeries.single_zero_one (#14061) Before this change, 0 was interpreted as a natural number.

Estimated changes

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

modified theorem HahnSeries.single_zero_one

Modified Mathlib/RingTheory/LaurentSeries.lean