lt_mul_of_le_of_one_lt'

Stream: mathlib4

[Kevin Buzzard]

docs#lt_mul_of_le_of_one_lt' has hypotheses 1 < a and 0 \le a. Is this an oversight or does the former really not always imply the latter?

[Andrew Yang]

It only requires Zero α so "0" can be an arbitrary (non-neg) element.

[Yuyang Zhao]

#9250 will remove it.

[Yuyang Zhao]

The first PR that tried to remove it was almost 2 years ago.

[Yuyang Zhao]

(and #9904 is also as ancient as it is)