[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
⊢ q = 0 ∨ IsPrimePow q
[PROOFSTEP]
apply or_iff_not_imp_left.2
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
⊢ ¬q = 0 → IsPrimePow q
[PROOFSTEP]
intro q_pos
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
⊢ IsPrimePow q
[PROOFSTEP]
let K := LocalRing.ResidueField R
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
⊢ IsPrimePow q
[PROOFSTEP]
haveI RM_char := ringChar.charP K
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
⊢ IsPrimePow q
[PROOFSTEP]
let r := ringChar K
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
⊢ IsPrimePow q
[PROOFSTEP]
let n := q.factorization r
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
⊢ IsPrimePow q
[PROOFSTEP]
cases' CharP.char_is_prime_or_zero K r with r_prime r_zero
[GOAL]
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
⊢ IsPrimePow q
[PROOFSTEP]
let a := q / r ^ n
[GOAL]
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
⊢ IsPrimePow q
[PROOFSTEP]
have q_eq_a_mul_rn : q = r ^ n * a := by rw [Nat.mul_div_cancel' (Nat.ord_proj_dvd q r)]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
⊢ q = r ^ n * a
[PROOFSTEP]
rw [Nat.mul_div_cancel' (Nat.ord_proj_dvd q r)]
[GOAL]
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = r ^ n * a
⊢ IsPrimePow q
[PROOFSTEP]
have r_ne_dvd_a := Nat.not_dvd_ord_compl r_prime q_pos
[GOAL]
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = r ^ n * a
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
⊢ IsPrimePow q
[PROOFSTEP]
have rn_dvd_q : r ^ n ∣ q := ⟨a, q_eq_a_mul_rn⟩
[GOAL]
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = r ^ n * a
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
⊢ IsPrimePow q
[PROOFSTEP]
rw [mul_comm] at q_eq_a_mul_rn 
[GOAL]
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
⊢ IsPrimePow q
[PROOFSTEP]
have a_unit : IsUnit (a : R) := by
  by_contra g
  rw [← mem_nonunits_iff] at g 
  rw [← LocalRing.mem_maximalIdeal] at g 
  have a_cast_zero := Ideal.Quotient.eq_zero_iff_mem.2 g
  rw [map_natCast] at a_cast_zero 
  have r_dvd_a := (ringChar.spec K a).1 a_cast_zero
  exact absurd r_dvd_a r_ne_dvd_a
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
⊢ IsUnit ↑a
[PROOFSTEP]
by_contra g
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
g : ¬IsUnit ↑a
⊢ False
[PROOFSTEP]
rw [← mem_nonunits_iff] at g 
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
g : ↑a ∈ nonunits R
⊢ False
[PROOFSTEP]
rw [← LocalRing.mem_maximalIdeal] at g 
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
g✝ : ↑a ∈ nonunits R
g : ↑a ∈ LocalRing.maximalIdeal R
⊢ False
[PROOFSTEP]
have a_cast_zero := Ideal.Quotient.eq_zero_iff_mem.2 g
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
g✝ : ↑a ∈ nonunits R
g : ↑a ∈ LocalRing.maximalIdeal R
a_cast_zero : ↑(Ideal.Quotient.mk (LocalRing.maximalIdeal R)) ↑a = 0
⊢ False
[PROOFSTEP]
rw [map_natCast] at a_cast_zero 
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
g✝ : ↑a ∈ nonunits R
g : ↑a ∈ LocalRing.maximalIdeal R
a_cast_zero : ↑a = 0
⊢ False
[PROOFSTEP]
have r_dvd_a := (ringChar.spec K a).1 a_cast_zero
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
g✝ : ↑a ∈ nonunits R
g : ↑a ∈ LocalRing.maximalIdeal R
a_cast_zero : ↑a = 0
r_dvd_a : ringChar K ∣ a
⊢ False
[PROOFSTEP]
exact absurd r_dvd_a r_ne_dvd_a
[GOAL]
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit ↑a
⊢ IsPrimePow q
[PROOFSTEP]
cases' a_unit.exists_left_inv with a_inv h_inv_mul_a
[GOAL]
case inl.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit ↑a
a_inv : R
h_inv_mul_a : a_inv * ↑a = 1
⊢ IsPrimePow q
[PROOFSTEP]
have rn_cast_zero : ↑(r ^ n) = (0 : R) :=
  by
  rw [← @mul_one R _ (r ^ n), mul_comm, ← Classical.choose_spec a_unit.exists_left_inv, mul_assoc, ← Nat.cast_mul, ←
    q_eq_a_mul_rn, CharP.cast_eq_zero R q]
  simp
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit ↑a
a_inv : R
h_inv_mul_a : a_inv * ↑a = 1
⊢ ↑(r ^ n) = 0
[PROOFSTEP]
rw [← @mul_one R _ (r ^ n), mul_comm, ← Classical.choose_spec a_unit.exists_left_inv, mul_assoc, ← Nat.cast_mul, ←
  q_eq_a_mul_rn, CharP.cast_eq_zero R q]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit ↑a
a_inv : R
h_inv_mul_a : a_inv * ↑a = 1
⊢ Classical.choose (_ : ∃ b, b * ↑a = 1) * 0 = 0
[PROOFSTEP]
simp
[GOAL]
case inl.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit ↑a
a_inv : R
h_inv_mul_a : a_inv * ↑a = 1
rn_cast_zero : ↑(r ^ n) = 0
⊢ IsPrimePow q
[PROOFSTEP]
have q_eq_rn := Nat.dvd_antisymm ((CharP.cast_eq_zero_iff R q (r ^ n)).mp rn_cast_zero) rn_dvd_q
[GOAL]
case inl.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit ↑a
a_inv : R
h_inv_mul_a : a_inv * ↑a = 1
rn_cast_zero : ↑(r ^ n) = 0
q_eq_rn : q = r ^ n
⊢ IsPrimePow q
[PROOFSTEP]
have n_pos : n ≠ 0 := fun n_zero =>
  absurd (by simpa [n_zero] using q_eq_rn)
    (CharP.char_ne_one R q)
      -- Definition of prime power: `∃ r n, Prime r ∧ 0 < n ∧ r ^ n = q`.
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit ↑a
a_inv : R
h_inv_mul_a : a_inv * ↑a = 1
rn_cast_zero : ↑(r ^ n) = 0
q_eq_rn : q = r ^ n
n_zero : n = 0
⊢ q = 1
[PROOFSTEP]
simpa [n_zero] using q_eq_rn
[GOAL]
case inl.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ ↑(Nat.factorization q) r
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit ↑a
a_inv : R
h_inv_mul_a : a_inv * ↑a = 1
rn_cast_zero : ↑(r ^ n) = 0
q_eq_rn : q = r ^ n
n_pos : n ≠ 0
⊢ IsPrimePow q
[PROOFSTEP]
exact ⟨r, ⟨n, ⟨r_prime.prime, ⟨pos_iff_ne_zero.mpr n_pos, q_eq_rn.symm⟩⟩⟩⟩
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_zero : r = 0
⊢ IsPrimePow q
[PROOFSTEP]
haveI K_char_p_0 := ringChar.of_eq r_zero
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_zero : r = 0
K_char_p_0 : CharP K 0
⊢ IsPrimePow q
[PROOFSTEP]
haveI K_char_zero : CharZero K := CharP.charP_to_charZero K
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_zero : r = 0
K_char_p_0 : CharP K 0
K_char_zero : CharZero K
⊢ IsPrimePow q
[PROOFSTEP]
haveI R_char_zero :=
  RingHom.charZero
    (LocalRing.residue R)
      -- Finally, `r = 0` would lead to a contradiction:
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_zero : r = 0
K_char_p_0 : CharP K 0
K_char_zero : CharZero K
R_char_zero : CharZero R
⊢ IsPrimePow q
[PROOFSTEP]
have q_zero := CharP.eq R char_R_q (CharP.ofCharZero R)
[GOAL]
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := LocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : (fun x => ℕ) r := ↑(Nat.factorization q) r
r_zero : r = 0
K_char_p_0 : CharP K 0
K_char_zero : CharZero K
R_char_zero : CharZero R
q_zero : q = 0
⊢ IsPrimePow q
[PROOFSTEP]
exact absurd q_zero q_pos
