Commit 2025-12-06 18:41 50d7b2ce

View on Github →

chore: dualize WithBot and WithTop using to_dual (#32488)

Estimated changes

modified def WithBot.some
deleted def WithTop.recTopCoe
deleted theorem WithTop.recTopCoe_coe
deleted theorem WithTop.recTopCoe_top
deleted def WithTop.some
deleted def WithTop