mathlib

790ec6b1 - feat(algebra/archimedean): rat.cast_round for non-archimedean fields (#7424)

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.