Commit 75f9e888 authored by MARCHE Claude's avatar MARCHE Claude

fix type error in algebra

parent 7efae3f8
......@@ -90,15 +90,15 @@ theory Field
axiom Inverse : forall x:t. x <> zero -> x * inv x = one
function (/) (x y : t) : t = x * inv y
lemma assoc_mul_div: forall x y z:real.
lemma assoc_mul_div: forall x y z:t.
(* todo: discard the hypothesis ? *)
z <> zero -> (x*y)/z = x*(y/z)
lemma assoc_div_mul: forall x y z:real.
lemma assoc_div_mul: forall x y z:t.
(* todo: discard the hypothesis ? *)
y <> zero /\ z <> zero -> (x/y)/z = x/(y*z)
lemma assoc_div_div: forall x y z:real.
lemma assoc_div_div: forall x y z:t.
(* todo: discard the hypothesis ? *)
y <> zero /\ z <> zero -> x/(y/z) = (x*z)/y
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment