Commit 2025-07-30 02:14 ea18d065

View on Github →

feat: With{Bot,Top}.map_injective (#27651) Using Option.map_injective in downstream code would be defeq abuse.

Estimated changes

added theorem WithBot.map_injective
added theorem WithTop.map_injective