Library Coq.setoid_ring.Integral_domain
Require
Export
Cring
.
Class
Integral_domain
{
R
:
Type
}`{
Rcr
:
Cring
R
} := {
integral_domain_product
:
forall
x
y
,
x
*
y
==
0
->
x
==
0
\/
y
==
0;
integral_domain_one_zero
:
not
(1
==
0)}.
Section
integral_domain
.
Context
{
R
:
Type
}`{
Rid
:
Integral_domain
R
}.
Lemma
integral_domain_minus_one_zero
:
~
-
(
1:
R
)
==
0.
Definition
pow
(
r
:
R
) (
n
:
nat
) :=
Ring_theory.pow_N
1
mul
r
(
N.of_nat
n
).
Lemma
pow_not_zero
:
forall
p
n
,
pow
p
n
==
0
->
p
==
0.
Lemma
Rintegral_domain_pow
:
forall
c
p
r
,
~
c
==
0
->
c
*
(
pow
p
r
)
==
ring0
->
p
==
ring0
.
End
integral_domain
.