-
Notifications
You must be signed in to change notification settings - Fork 298
/
nat_prime.lean
39 lines (33 loc) · 1.48 KB
/
nat_prime.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
/-
Copyright (c) 2020 Bryan Gin-ge Chen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kevin Lacker, Bryan Gin-ge Chen
-/
import data.nat.prime
import data.int.basic
/-!
# Lemmas about nat.prime using `int`s
-/
open nat
namespace int
lemma not_prime_of_int_mul {a b : ℤ} {c : ℕ}
(ha : 1 < a.nat_abs) (hb : 1 < b.nat_abs) (hc : a*b = (c : ℤ)) : ¬ nat.prime c :=
not_prime_mul' (nat_abs_mul_nat_abs_eq hc) ha hb
lemma 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 :=
have hpm' : p ^ k ∣ m.nat_abs, from int.coe_nat_dvd.1 $ int.dvd_nat_abs.2 hpm,
have hpn' : p ^ l ∣ n.nat_abs, from int.coe_nat_dvd.1 $ int.dvd_nat_abs.2 hpn,
have hpmn' : (p ^ (k+l+1)) ∣ m.nat_abs*n.nat_abs,
by rw ←int.nat_abs_mul; apply (int.coe_nat_dvd.1 $ int.dvd_nat_abs.2 hpmn),
let hsd := nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul p_prime hpm' hpn' hpmn' in
hsd.elim
(λ hsd1, or.inl begin apply int.dvd_nat_abs.1, apply int.coe_nat_dvd.2 hsd1 end)
(λ hsd2, or.inr begin apply int.dvd_nat_abs.1, apply int.coe_nat_dvd.2 hsd2 end)
lemma prime.dvd_nat_abs_of_coe_dvd_sq {p : ℕ} (hp : p.prime) (k : ℤ) (h : ↑p ∣ k ^ 2) :
p ∣ k.nat_abs :=
begin
apply @nat.prime.dvd_of_dvd_pow _ _ 2 hp,
rwa [sq, ← nat_abs_mul, ← coe_nat_dvd_left, ← sq]
end
end int