R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
⊢ ¬q = 0 → IsPrimePow q
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
⊢ q = 0 ∨ IsPrimePow q
apply or_iff_not_imp_left.2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
⊢ IsPrimePow q
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
⊢ ¬q = 0 → IsPrimePow q
intro q_pos
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
R : Type u_1
inst✝¹ : CommRing R
inst✝ : LocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
⊢ IsPrimePow q
let K := LocalRing.ResidueField R
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
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
haveI RM_char := ringChar.charP K
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
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
let r := ringChar K
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
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
let n := q.factorization r
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

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
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
cases' CharP.char_is_prime_or_zero K r with r_prime r_zero
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
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
let a := q / r ^ n
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
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
have q_eq_a_mul_rn : q = r ^ n * a := by rw [Nat.mul_div_cancel' (Nat.ord_proj_dvd q r)]
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
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
have r_ne_dvd_a := Nat.not_dvd_ord_compl r_prime q_pos
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
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
have rn_dvd_q : r ^ n ∣ q := ⟨a, q_eq_a_mul_rn⟩
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
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
rw [mul_comm] at q_eq_a_mul_rn
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
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
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
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
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
cases' a_unit.exists_left_inv with a_inv h_inv_mul_a
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
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
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
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
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
have q_eq_rn := Nat.dvd_antisymm ((CharP.cast_eq_zero_iff R q (r ^ n)).mp rn_cast_zero) rn_dvd_q
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
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
have n_pos : n ≠ 0 := fun n_zero =>
  absurd (by simpa [n_zero] using q_eq_rn) (CharP.char_ne_one R q)
no goals
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
exact ⟨r, ⟨n, ⟨r_prime.prime, ⟨pos_iff_ne_zero.mpr n_pos, q_eq_rn.symm⟩⟩⟩⟩
no goals
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
rw [Nat.mul_div_cancel' (Nat.ord_proj_dvd q r)]
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
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
by_contra g
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
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
rw [← mem_nonunits_iff] at g
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
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
rw [← LocalRing.mem_maximalIdeal] at g
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
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
have a_cast_zero := Ideal.Quotient.eq_zero_iff_mem.2 g
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
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
rw [map_natCast] at a_cast_zero
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
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
have r_dvd_a := (ringChar.spec K a).1 a_cast_zero
no goals
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
exact absurd r_dvd_a r_ne_dvd_a
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
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
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]
no goals
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
simp
no goals
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
simpa [n_zero] using q_eq_rn
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
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
haveI K_char_p_0 := ringChar.of_eq r_zero
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
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
haveI K_char_zero : CharZero K := CharP.charP_to_charZero K
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
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
haveI R_char_zero := RingHom.charZero (LocalRing.residue R)
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
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
have q_zero := CharP.eq R char_R_q (CharP.ofCharZero R)
no goals
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
exact absurd q_zero q_pos