Commit 2024-12-20 10:20 25ee8b01

View on Github →

feat(Algebra/Order/Monoid/Unbundled/WithTop): add lemmas about WithTop.map and WithBot.map (#19122)

Estimated changes

added theorem WithBot.map_eq_one_iff
added theorem WithBot.map_natCast
added theorem WithBot.map_ofNat
added theorem WithBot.one_eq_map_iff
added theorem WithTop.map_eq_one_iff
added theorem WithTop.map_natCast
added theorem WithTop.map_ofNat
added theorem WithTop.one_eq_map_iff