From 0ceac44dc7459370c069753ad469cab47b61701d Mon Sep 17 00:00:00 2001 From: Alex J Best Date: Sun, 19 Apr 2020 01:55:09 +0000 Subject: [PATCH] feat(data/nat/prime) factors of a prime number is the list [p] (#2452) The factors of a prime number are [p]. Co-authored-by: Scott Morrison --- src/data/nat/prime.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/data/nat/prime.lean b/src/data/nat/prime.lean index 803eadc223a25..2de92d0b60ac6 100644 --- a/src/data/nat/prime.lean +++ b/src/data/nat/prime.lean @@ -315,6 +315,17 @@ lemma prod_factors : ∀ {n}, 0 < n → list.prod (factors n) = n by rw zero_mul at this; exact (show k + 2 ≠ 0, from dec_trivial) this, by rw [list.prod_cons, prod_factors h₁, nat.mul_div_cancel' (min_fac_dvd _)] +lemma factors_prime {p : ℕ} (hp : nat.prime p) : p.factors = [p] := +begin + have : p = (p - 2) + 2 := (nat.sub_eq_iff_eq_add hp.1).mp rfl, + rw [this, nat.factors], + simp only [eq.symm this], + have : nat.min_fac p = p := (nat.prime_def_min_fac.mp hp).2, + split, + { exact this, }, + { simp only [this, nat.factors, nat.div_self (nat.prime.pos hp)], }, +end + theorem prime.coprime_iff_not_dvd {p n : ℕ} (pp : prime p) : coprime p n ↔ ¬ p ∣ n := ⟨λ co d, pp.not_dvd_one $ co.dvd_of_dvd_mul_left (by simp [d]), λ nd, coprime_of_dvd $ λ m m2 mp, ((dvd_prime_two_le pp m2).1 mp).symm ▸ nd⟩