`ceil` are preserved under order ring homs (#16025)

Commit

4 years ago

feat(algebra/order/floor): `floor`/`ceil` are preserved under order ring homs (#16025) `⌊f a⌋ = ⌊a⌋`, `⌈f a⌉ = ⌈a⌉` and similar for `f` a strictly monotone ring homomorphism.

Author

YaelDillies

Parents

a9402e0a

mathlib3 fa0bbc79 - feat(algebra/order/floor): `floor`/`ceil` are preserved under order ring homs (#16025)

mathlib3
fa0bbc79 - feat(algebra/order/floor): `floor`/`ceil` are preserved under order ring homs (#16025)