Commit 2026-03-08 06:01 06e94735

View on Github →

chore(Order/Hom/Lattice): use to_dual (#36159)

Estimated changes

deleted theorem InfHom.bot_apply
deleted theorem InfHom.cancel_left
deleted theorem InfHom.cancel_right
deleted theorem InfHom.coe_bot
deleted theorem InfHom.coe_comp
deleted theorem InfHom.coe_const
deleted theorem InfHom.coe_copy
deleted theorem InfHom.coe_id
deleted theorem InfHom.coe_inf
deleted theorem InfHom.coe_mk
deleted theorem InfHom.coe_top
deleted def InfHom.comp
deleted theorem InfHom.comp_apply
deleted theorem InfHom.comp_assoc
deleted theorem InfHom.comp_id
deleted def InfHom.const
deleted theorem InfHom.const_apply
deleted theorem InfHom.copy_eq
deleted theorem InfHom.dual_comp
deleted theorem InfHom.dual_id
deleted theorem InfHom.ext
deleted theorem InfHom.id_apply
deleted theorem InfHom.id_comp
deleted theorem InfHom.inf_apply
modified theorem InfHom.mk_le_mk
deleted theorem InfHom.symm_dual_comp
deleted theorem InfHom.symm_dual_id
deleted theorem InfHom.toFun_eq_coe
deleted theorem InfHom.top_apply
deleted theorem LatticeHom.coe_toInfHom
modified theorem LatticeHom.coe_toSupHom
modified theorem SupHom.coe_mk
modified theorem SupHom.comp_id
modified theorem SupHom.id_comp
modified theorem SupHom.toFun_eq_coe