Commit 2026-03-08 15:07 eda3563a

View on Github →

chore(Order/Hom/Bounded): use to_dual (#36354)

Estimated changes

deleted theorem BotHom.bot_apply
deleted theorem BotHom.cancel_left
deleted theorem BotHom.cancel_right
deleted theorem BotHom.coe_bot
deleted theorem BotHom.coe_comp
deleted theorem BotHom.coe_copy
deleted theorem BotHom.coe_id
deleted theorem BotHom.coe_inf
deleted theorem BotHom.coe_sup
deleted def BotHom.comp
deleted theorem BotHom.comp_apply
deleted theorem BotHom.comp_assoc
deleted theorem BotHom.comp_id
deleted theorem BotHom.copy_eq
deleted theorem BotHom.dual_comp
deleted theorem BotHom.dual_id
deleted theorem BotHom.ext
deleted theorem BotHom.id_apply
deleted theorem BotHom.id_comp
deleted theorem BotHom.inf_apply
deleted theorem BotHom.sup_apply
deleted theorem BotHom.symm_dual_comp
deleted theorem BotHom.symm_dual_id
deleted theorem map_eq_bot_iff