Commit 2025-06-09 11:40 eb04d3df
View on Github →fix(HahnSeries): solve SMul Rat
diamonds, and lemmas about casts (#25413)
This fixes the instances diamonds in the Rat
and NNRat
actions, and adds lemmas about {Nat,Int,NNRat,NRat}.cast
and of{Nat,Scientific}
.
There is no motivation here beyond cleaning up diamonds.