Commit 2022-08-29 08:18 9c0a5431

feat(counterexamples/map_floor): floor/ceil are not preserved under order ring homs (#16198) #16025 proves that ⌊f a⌋ = ⌊a⌋ and ⌈f a⌉ = ⌈a⌉ for a strictly monotone ring hom f. This counterexample shows that this can't be relaxed to f monotone.