primes in nat and int

Stream: Is there code for X?

[Damiano Testa]

Dear All,

I have been playing around with getting Lean to prove (in)solubility of certain simple polynomial equations and I found the lemmas below useful. Do you think that some of these lemmas are reasonable additions to mathlib?

Thanks!

[Damiano Testa]

import ring_theory.unique_factorization_domain
import ring_theory.int.basic

variables {α : Type*} {a b : α}

section ring
variables [ring α]

@[simp]
lemma associated.neg_left : associated (- a) b ↔ associated a b :=
begin
  refine ⟨λ h, _, λ h, _⟩;
  { cases h with u hu,
    exact ⟨- u, by simpa using hu⟩ }
end

@[simp]
lemma associated.neg_right : associated a (- b) ↔ associated a b :=
begin
  refine ⟨λ h, _, λ h, _⟩,
  { exact associated.symm (associated.neg_left.mp (associated.symm h)) },
  { exact associated.symm (associated.neg_left.mpr (associated.symm h)) }
end

end ring

/- As you can see from the proof, the forward direction already exists.
The point of this lemma is to have the iff version. -/
lemma prime.dvd_pow_iff [comm_monoid_with_zero α] {p : α} {n : ℕ}
  (a : α) (pp : prime p) (n0 : 0 < n) :
  p ∣ a ^ n ↔ p ∣ a :=
begin
  refine ⟨λ h, prime.dvd_of_dvd_pow pp h, λ h, _⟩,
  rcases h with ⟨a', rfl⟩,
  refine ⟨a' * (p * a') ^ n.pred, _⟩,
  rw [← nat.succ_pred_eq_of_pos n0] { occs := occurrences.pos [1] },
  rw [pow_succ, mul_assoc],
end

section comm_ring
variable [comm_ring α]

@[simp]
lemma associated.unit_left {u : units α} : associated (↑u * a) b ↔ associated a b :=
begin
  refine ⟨λ h, _, λ h, _⟩,
  { cases h with v hv,
    exact ⟨u * v, by rwa [units.coe_mul, ← mul_assoc, mul_comm a] ⟩ },
  { cases h with v hv,
    exact ⟨u⁻¹ * v, by rwa [mul_comm _ a, mul_assoc, ← units.coe_mul, mul_inv_cancel_left u v]⟩ }
end

@[simp]
lemma associated.unit_right {u : units α} : associated a (u * b) ↔ associated a b :=
begin
  refine ⟨λ h, _, λ h, _⟩,
  { exact associated.symm (associated.unit_left.mp (associated.symm h)) },
  { exact associated.symm (associated.unit_left.mpr (associated.symm h)) }
end

lemma neg_prime_iff {p : α} : prime (- p) ↔ prime p :=
⟨ λ h, prime_of_associated (associated.neg_left.mpr (associated.refl p)) h,
  λ h, prime_of_associated (associated.neg_right.mpr (associated.refl p)) h⟩

end comm_ring

lemma int.is_unit_coe {a : ℕ} : is_unit (a : ℤ) ↔ a = 1 :=
begin
  refine int.is_unit_iff.trans ⟨λ h, _, λ h, by exact_mod_cast or.inl h⟩,
  cases h,
  { exact_mod_cast h },
  { exact int.no_confusion h }
end

lemma int.irreducible_coe_iff {p : ℕ} : irreducible (p : ℤ) ↔ irreducible p :=
begin
  rw [irreducible_iff, irreducible_iff, nat.is_unit_iff, int.is_unit_coe],
  refine ⟨_, _⟩; rintros ⟨pu, pmul⟩; refine ⟨pu, λ a b ab, _⟩,
  { simpa [int.is_unit_coe] using pmul ↑a ↑b (by exact_mod_cast ab) },
  { simpa [int.is_unit_iff, nat.is_unit_iff, int.nat_abs_eq_iff]
      using pmul a.nat_abs b.nat_abs ((int.nat_abs_mul_nat_abs_eq ab.symm).symm) }
end

lemma int.prime_coe_iff {p : ℕ} : prime (p : ℤ) ↔ prime p :=
gcd_monoid.irreducible_iff_prime.symm.trans
  (int.irreducible_coe_iff.trans
    ((irreducible_iff_nat_prime _).trans
      nat.prime_iff_prime))

lemma int.prime_iff_nat_abs (p : ℤ) : prime p ↔ prime (int.nat_abs p) :=
begin
  refine iff.trans _ int.prime_coe_iff,
  cases p.nat_abs_eq; nth_rewrite 0 h,
  exact neg_prime_iff,
end

lemma int.prime_two : prime (2 : ℤ) :=
int.prime_coe_iff.mpr (nat.prime_iff.mp nat.prime_two)

lemma int.even_pow_iff (a : ℤ) {n : ℕ} (n0 : 0 < n) : even (a ^ n) ↔ even a :=
prime.dvd_pow_iff a int.prime_two n0

lemma int.even_sq_iff (a : ℤ) : even (a ^ 2) ↔ even a :=
prime.dvd_pow_iff a int.prime_two zero_lt_two

lemma int.coe_prime_iff_nat_prime {a : ℕ} : prime (a : ℤ) ↔ nat.prime a :=
int.prime_coe_iff.trans nat.prime_iff.symm

@[simp]
lemma even_zero [semiring α] : even (0 : α) := ⟨(0 : α), (mul_zero _).symm⟩

[Ruben Van de Velde]

Some of those are pretty close to existing lemmas:

lemma int.prime_coe_iff {p : ℕ} : prime (p : ℤ) ↔ prime p :=
nat.prime_iff_prime_int.symm.trans nat.prime_iff_prime

lemma int.prime_iff_nat_abs (p : ℤ) : prime p ↔ prime (int.nat_abs p) :=
int.prime_iff_nat_abs_prime.trans $ nat.prime_iff_prime_int.trans int.prime_coe_iff

lemma int.coe_prime_iff_nat_prime {a : ℕ} : prime (a : ℤ) ↔ nat.prime a :=
nat.prime_iff_prime_int.symm

[Damiano Testa]

Ruben, thank you very much! I commented out two of the lemmas from my list and shortened a proof using yours.

I am temporarily keeping int.prime_coe_iff {p : ℕ} : prime (p : ℤ) ↔ prime p, since I feel that converting a natural prime to an integer prime is a common enough operation and having a direct lemma for it seem reasonable.

Anywa, thanks again!

[Damiano Testa]

(deleted)

[Ruben Van de Velde]

I wonder if there's a reason to keep nat.prime and prime \N

[Damiano Testa]

I would be in favour of this, or at least renaming nat.prime to something closer to the definition: I personally found it tricky to navigate and had to constantly remind myself of which definition was which. I think that prime and irreducible are fairly standard, while nat.prime kept confusing me.