diff options
Diffstat (limited to 'src/Algebra.v')
-rw-r--r-- | src/Algebra.v | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index 6dc188e2c..eacc2b8bb 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -420,12 +420,20 @@ Module IntegralDomain. Context {T eq zero one opp add sub mul} `{@integral_domain T eq zero one opp add sub mul}. Lemma mul_nonzero_nonzero_cases (x y : T) - : eq (mul x y) zero -> eq x zero \/ eq y zero. + : eq (mul x y) zero -> eq x zero \/ eq y zero. Proof. pose proof mul_nonzero_nonzero x y. destruct (eq_dec x zero); destruct (eq_dec y zero); intuition. Qed. + Lemma mul_nonzero_nonzero_and (x y : T) + : ~eq (mul x y) zero -> ~eq x zero /\ ~eq y zero. + Proof. + intro H0; split; intro H1; apply H0; rewrite H1. + { apply Ring.mul_0_r. } + { apply Ring.mul_0_l. } + Qed. + Global Instance Integral_domain : @Integral_domain.Integral_domain T zero one add mul sub opp eq Ring.Ncring_Ring_ops Ring.Ncring_Ring Ring.Cring_Cring_commutative_ring. |