Re: [isabelle] Inequality assumption
In Isabelle/HOL, we are having a definition that x/0=0:
assumes inverse_zero [simp]: "inverse 0 = 0"
in this case, divide_right_mono holds as a/0 = b/0 = 0, but whether this
makes sense to mathematician is another question...
On 2016-07-05 16:22, Omar Jasim wrote:
I've seen this lemma in Fields theory:
"[|a â b; 0 â c|] ==> a/c â b/c"
by (force simp add: divide_strict_right_mono le_less)
here 0 â c which I think it should be 0 < c as the division cann't done
University of Cambridge
This archive was generated by a fusion of
Pipermail (Mailman edition) and