Commit 2026-05-06 19:54 bedd3945

View on Github →

feat: IsBotOneClass and IsBotZeroClass (#38730) We create typeclasses expressing that 0 or 1 is a bottom element in a type. We use this to unify and generalize various theorems which are currently stated for canonically ordered monoids. This has provisionally left us with a bunch of unnecessary aliases; these will be deprecated in a follow-up PR (tentatively #38663). See Zulip.

Estimated changes

modified theorem WithZero.zero_le
deleted theorem bot_eq_zero''
deleted theorem le_zero_iff
deleted theorem ne_zero_of_lt
deleted theorem not_lt_zero'
modified theorem pow_pos_iff
deleted theorem zero_le'
deleted theorem zero_lt_iff
added theorem NeZero.of_ge
added theorem NeZero.of_gt
added theorem NeZero.pos
added theorem bot_eq_one
added theorem eq_one_or_one_lt
added theorem isBot_one
added theorem le_one_iff_eq_one
added theorem min_one
added theorem ne_one_of_lt
added theorem not_lt_one
added theorem one_le
added theorem one_lt_iff_ne_one
added theorem one_lt_of_gt
added theorem one_min
added theorem one_notMem_iff
deleted theorem Left.one_lt_mul_of_left
deleted theorem Left.one_lt_mul_of_right
deleted theorem NeZero.of_ge
deleted theorem NeZero.of_gt
deleted theorem NeZero.pos
deleted theorem Right.one_lt_mul_of_left
deleted theorem Right.one_lt_mul_of_right
deleted theorem bot_eq_one
deleted theorem eq_one_or_one_lt
deleted theorem isBot_one
deleted theorem le_one_iff_eq_one
deleted theorem min_one
deleted theorem ne_one_of_lt
deleted theorem not_lt_one
deleted theorem one_le
deleted theorem one_lt_iff_ne_one
deleted theorem one_lt_of_gt
deleted theorem one_lt_of_ne_one
deleted theorem one_min
deleted theorem one_notMem_iff