Documentation
Mathlib
.
Data
.
Int
.
NatPrime
Search
return to top
source
Imports
Init
Mathlib.Data.Int.Basic
Mathlib.Algebra.Group.Int.Defs
Mathlib.Data.Nat.Prime.Basic
Imported by
Int
.
not_prime_of_int_mul
Int
.
succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul
Int
.
Prime
.
dvd_natAbs_of_coe_dvd_sq
Lemmas about
Nat.Prime
using
Int
s
#
source
theorem
Int
.
not_prime_of_int_mul
{
a
b
:
Int
}
{
c
:
Nat
}
(
ha
:
Ne
a
.
natAbs
1
)
(
hb
:
Ne
b
.
natAbs
1
)
(
hc
:
Eq
(
HMul.hMul
a
b
)
c
.
cast
)
:
Not
(
Nat.Prime
c
)
source
theorem
Int
.
succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul
{
p
:
Nat
}
(
p_prime
:
Nat.Prime
p
)
{
m
n
:
Int
}
{
k
l
:
Nat
}
(
hpm
:
Dvd.dvd
(
HPow.hPow
p
k
)
.
cast
m
)
(
hpn
:
Dvd.dvd
(
HPow.hPow
p
l
)
.
cast
n
)
(
hpmn
:
Dvd.dvd
(
HPow.hPow
p
(
HAdd.hAdd
(
HAdd.hAdd
k
l
)
1
)
)
.
cast
(
HMul.hMul
m
n
)
)
:
Or
(
Dvd.dvd
(
HPow.hPow
p
(
HAdd.hAdd
k
1
)
)
.
cast
m
)
(
Dvd.dvd
(
HPow.hPow
p
(
HAdd.hAdd
l
1
)
)
.
cast
n
)
source
theorem
Int
.
Prime
.
dvd_natAbs_of_coe_dvd_sq
{
p
:
Nat
}
(
hp
:
Nat.Prime
p
)
(
k
:
Int
)
(
h
:
Dvd.dvd
p
.
cast
(
HPow.hPow
k
2
)
)
:
Dvd.dvd
p
k
.
natAbs