Zulip Chat Archive

Stream: maths

Topic: linear_ordered_semiring theorems


view this post on Zulip Mario Carneiro (May 03 2020 at 06:20):

zero_lt_two, one_lt_two, lt_add_one, lt_one_add, bit1_pos, one_lt_mul, mul_le_one, one_lt_mul_of_le_of_lt, and several others all assume linear_ordered_semiring, while the linear order does not appear necessary here since there is no multiplicative cancellation going on

view this post on Zulip Mario Carneiro (May 03 2020 at 06:22):

(While I'm at it, now's the time to suggest weaker typeclass assumptions on the core norm_num theorems. I know that there was a problem with working with division in complex because it makes unjustified linear order assumptions, and I haven't addressed that yet.)


Last updated: May 12 2021 at 08:14 UTC