Commit 2025-08-26 15:11 e6872973

View on Github →

chore: define WithZero order instances without reference to WithBot (#28957)

Estimated changes

deleted def WithOne.map
added theorem WithOne.mapMulHom_coe
added theorem WithOne.mapMulHom_comp
added theorem WithOne.mapMulHom_id
added theorem WithOne.mapMulHom_inj
deleted theorem WithOne.map_coe
deleted theorem WithOne.map_comp
deleted theorem WithOne.map_id
deleted theorem WithOne.map_inj
deleted theorem WithOne.map_injective'
deleted theorem WithOne.map_injective
deleted theorem WithOne.map_map
added def WithOne.map
added theorem WithOne.map_bot
added theorem WithOne.map_coe
added def WithOne.map₂
added theorem WithOne.map₂_coe_coe
added theorem WithZero.coe_inf
modified theorem WithZero.coe_le_coe
modified theorem WithZero.coe_le_iff
modified theorem WithZero.coe_lt_coe
added theorem WithZero.coe_sup
added theorem WithZero.le_def
added theorem WithZero.lt_def
modified theorem WithZero.not_coe_le_zero
deleted theorem WithZero.not_lt_zero
modified theorem WithZero.zero_le
modified theorem WithZero.zero_lt_coe