Commit 2021-05-01 15:16 790ec6b1
View on Github →feat(algebra/archimedean): rat.cast_round for non-archimedean fields (#7424)
The theorem still applies to the non-canonical archimedean instance (at least if you use simp). I've also added rat.cast_ceil because it seems to fit here.