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}.castand of{Nat,Scientific}. There is no motivation here beyond cleaning up diamonds.

Estimated changes