prime factorisation

Stream: Is there code for X?

[Jon Eugster]

I'm having a bit troubles with factorisations/multiplicity. Could somebody help me proving the statement below, which just says that I can write the factorisation of $q \in \mathbb{N}$ as $q =a r^n$ for any prime factor $r$:

import ring_theory.ideal.local_ring
import algebra.char_p

example (q r:ℕ) (h: r ∣ q) (hr: nat.prime r): ∃(a n:ℕ), q = a*r^n ∧ ¬(r ∣ a) := begin
  -- Proof:
  -- Write the factorisation of `q = r^n * r_1^n_1 * ... * r_m ^ n_m`
  -- and set `a := r_1^n_1 * ... * r_m ^ n_m`.
  -- By definition it should be obvious that `¬(r ∣ a)`.
  sorry,
end

Thanks for the help.

For context, I am working with local rings and want to say that for any prime ideal I we have char(R⧸I) = r^n where r := char(R⧸M). So roughly this boils down to the following statement which is a direct corollary of the above:

example (R: Type*) [comm_ring R] [local_ring R] (q: ℕ):
∃(a n: ℕ), q = a*(ring_char (local_ring.residue_field R))^n ∧ ↑a ∉ (local_ring.maximal_ideal R):= begin
  -- Proof:
  -- Set `r := ring_char (local_ring.residue_field R)` and
  -- use the above example to get `q = a*r^n`.
  -- Since `¬(r ∣ a)` we have that `(a:R⧸M) ≠ 0` so `(a:R) ∉ M`.
  sorry,
end

[Eric Rodriguez]

docs#nat.prime.pow_dvd_iff_le_factorization, docs#nat.pow_factorization_dvd, docs#nat.pow_succ_factorization_not_dvd should get you there

[Eric Rodriguez]

I find the last two of those are the most hlepful

[Eric Rodriguez]

oh, also docs#nat.factorization_div

[Stuart Presnell]

The following proof works, using a couple of auxiliary lemmas that I've PR'd at #14031

lemma pow_factorization_le {n : ℕ} (p : ℕ) (hn : 0 < n) : p ^ (n.factorization) p ≤ n :=
le_of_dvd hn (nat.pow_factorization_dvd n p)

lemma div_pow_factorization_ne_zero {n : ℕ} (p : ℕ) (hn : 0 < n) :
  n / p ^ (n.factorization) p ≠ 0 :=
begin
  by_cases pp : nat.prime p,
  { apply mt (nat.div_eq_zero_iff (pow_pos (prime.pos pp) _)).1,
    simp [le_of_dvd hn (nat.pow_factorization_dvd n p)] },
  { simp [nat.factorization_eq_zero_of_non_prime n pp, hn.ne'] },
end

lemma not_dvd_div_pow_factorization {n p : ℕ} (hp : prime p) (h: p ∣ n) (hn : 0 < n) :
  ¬p ∣ n / p ^ (n.factorization) p :=
begin
  rw [nat.prime.dvd_iff_one_le_factorization hp (div_pow_factorization_ne_zero p hn),
    nat.factorization_div (nat.pow_factorization_dvd n p)],
  simp [hp.factorization],
end

example (q r : ℕ) (h : r ∣ q) (hr : nat.prime r) (hq : 0 < q):
  ∃ a n : ℕ, q = a * r^n ∧ ¬(r ∣ a) :=
begin
  let i := q.factorization r,
  refine ⟨q/r^i, i, _, not_dvd_div_pow_factorization hr h hq⟩,
  rw [mul_comm, nat.mul_div_cancel' (nat.pow_factorization_dvd q r)],
end

[Stuart Presnell]

Also, just to note that you can drop the assumption (h : r ∣ q) and instead insert the following line at the start of the proof:

by_cases h : r ∣ q, swap, { use [q, 0], simp [h] },

[Jon Eugster]

Thank you Eric Rodriguez, especially nat.pow_factorization_dvd really helped to get going. And the full solution is amazing and Stuart Presnell , much apprechiated!