Theorem HahnSeries.single_zero_intCast

Modification history

2025-06-09 11:40
Mathlib/RingTheory/HahnSeries/Multiplication.lean
fix(HahnSeries): solve `SMul Rat` diamonds, and lemmas about casts (#25413) …
Added HahnSeries.single_zero_intCastView on Github →