mathlib

f73befff - feat(algebra/order/monoid): add lemmas `map_add` for `with_bot/top` (#15300)

feat(algebra/order/monoid): add lemmas `map_add` for `with_bot/top` (#15300) This PR shows that a map that preserves addition on a type with addition, also preserves addition on `with_bot/top`.