Commit 2025-11-03 16:36 d2abc004

View on Github →

refactor: define < on WithBot/WithTop as an inductive predicate (#30848) Follow up to #19668, where I did the same for LE but forgot to do it for LT.

Estimated changes

modified theorem WithZero.lt_coe_iff
modified theorem WithZero.lt_def
added theorem WithZero.lt_iff_exists
modified theorem WithBot.lt_coe_iff
modified theorem WithBot.lt_def
added theorem WithBot.lt_iff_exists
modified theorem WithTop.coe_lt_iff
modified theorem WithTop.lt_def
added theorem WithTop.lt_iff_exists