Documentation
Mathlib
.
Data
.
Int
.
NatPrime
Search
Google site search
return to top
source
Imports
Init
Mathlib.Algebra.Group.Int
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 :
ℤ
}
{c :
ℕ
}
(ha :
a
.natAbs
≠
1
)
(hb :
b
.natAbs
≠
1
)
(hc :
a
*
b
=
↑
c
)
:
¬
Nat.Prime
c
source
theorem
Int
.
succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul
{p :
ℕ
}
(p_prime :
Nat.Prime
p
)
{m n :
ℤ
}
{k l :
ℕ
}
(hpm :
↑
(
p
^
k
)
∣
m
)
(hpn :
↑
(
p
^
l
)
∣
n
)
(hpmn :
↑
(
p
^
(
k
+
l
+
1
)
)
∣
m
*
n
)
:
↑
(
p
^
(
k
+
1
)
)
∣
m
∨
↑
(
p
^
(
l
+
1
)
)
∣
n
source
theorem
Int
.
Prime
.
dvd_natAbs_of_coe_dvd_sq
{p :
ℕ
}
(hp :
Nat.Prime
p
)
(k :
ℤ
)
(h :
↑
p
∣
k
^
2
)
:
p
∣
k
.natAbs