Documentation
Mathlib
.
Data
.
Int
.
NatPrime
Search
Google site search
return to top
source
Imports
Init
Mathlib.Data.Nat.Prime
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
)
:
¬
c
.Prime
source
theorem
Int
.
succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul
{p :
ℕ
}
(p_prime :
p
.Prime
)
{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 :
p
.Prime
)
(k :
ℤ
)
(h :
↑
p
∣
k
^
2
)
:
p
∣
k
.natAbs