Theorem HahnSeries.single_zero_one
Modification history
2025-06-09 11:40
Mathlib/RingTheory/HahnSeries/Multiplication.lean
fix(HahnSeries): solve `SMul Rat` diamonds, and lemmas about casts (#25413) …
Modified HahnSeries.single_zero_oneView on Github →2024-06-24 10:09
Mathlib/RingTheory/HahnSeries/Multiplication.lean
fix: generalize HahnSeries.single_zero_one (#14061) …
Modified HahnSeries.single_zero_oneView on Github →