[GOAL]
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
⊢ IsUnit ↑p ↔ ¬p ∣ ringChar R
[PROOFSTEP]
have hch := CharP.cast_eq_zero R (ringChar R)
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
⊢ IsUnit ↑p ↔ ¬p ∣ ringChar R
[PROOFSTEP]
have hp : p.Prime := Fact.out
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
⊢ IsUnit ↑p ↔ ¬p ∣ ringChar R
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
⊢ IsUnit ↑p → ¬p ∣ ringChar R
[PROOFSTEP]
rintro h₁ ⟨q, hq⟩
[GOAL]
case mp.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
hq : ringChar R = p * q
⊢ False
[PROOFSTEP]
rcases IsUnit.exists_left_inv h₁ with ⟨a, ha⟩
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * ↑p = 1
⊢ False
[PROOFSTEP]
have h₃ : ¬ringChar R ∣ q := by
  rintro ⟨r, hr⟩
  rw [hr, ← mul_assoc, mul_comm p, mul_assoc] at hq 
  nth_rw 1 [← mul_one (ringChar R)] at hq 
  exact Nat.Prime.not_dvd_one hp ⟨r, mul_left_cancel₀ hR hq⟩
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * ↑p = 1
⊢ ¬ringChar R ∣ q
[PROOFSTEP]
rintro ⟨r, hr⟩
[GOAL]
case intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * ↑p = 1
r : ℕ
hr : q = ringChar R * r
⊢ False
[PROOFSTEP]
rw [hr, ← mul_assoc, mul_comm p, mul_assoc] at hq 
[GOAL]
case intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
r : ℕ
hq : ringChar R = ringChar R * (p * r)
hr : q = ringChar R * r
⊢ False
[PROOFSTEP]
nth_rw 1 [← mul_one (ringChar R)] at hq 
[GOAL]
case intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
r : ℕ
hq : ringChar R * 1 = ringChar R * (p * r)
hr : q = ringChar R * r
⊢ False
[PROOFSTEP]
exact Nat.Prime.not_dvd_one hp ⟨r, mul_left_cancel₀ hR hq⟩
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * ↑p = 1
h₃ : ¬ringChar R ∣ q
⊢ False
[PROOFSTEP]
have h₄ := mt (CharP.int_cast_eq_zero_iff R (ringChar R) q).mp
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * ↑p = 1
h₃ : ¬ringChar R ∣ q
h₄ : ¬↑(ringChar R) ∣ ↑q → ¬↑↑q = 0
⊢ False
[PROOFSTEP]
apply_fun ((↑) : ℕ → R) at hq 
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
h₃ : ¬ringChar R ∣ q
h₄ : ¬↑(ringChar R) ∣ ↑q → ¬↑↑q = 0
hq : ↑(ringChar R) = ↑(p * q)
⊢ False
[PROOFSTEP]
apply_fun (· * ·) a at hq 
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
h₃ : ¬ringChar R ∣ q
h₄ : ¬↑(ringChar R) ∣ ↑q → ¬↑↑q = 0
hq : a * ↑(ringChar R) = a * ↑(p * q)
⊢ False
[PROOFSTEP]
rw [Nat.cast_mul, hch, mul_zero, ← mul_assoc, ha, one_mul] at hq 
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
h₃ : ¬ringChar R ∣ q
h₄ : ¬↑(ringChar R) ∣ ↑q → ¬↑↑q = 0
hq : 0 = ↑q
⊢ False
[PROOFSTEP]
norm_cast at h₄ 
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
h₃ : ¬ringChar R ∣ q
hq : 0 = ↑q
h₄ : ¬ringChar R ∣ q → ¬↑q = 0
⊢ False
[PROOFSTEP]
exact h₄ h₃ hq.symm
[GOAL]
case mpr
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
⊢ ¬p ∣ ringChar R → IsUnit ↑p
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
⊢ IsUnit ↑p
[PROOFSTEP]
rcases(hp.coprime_iff_not_dvd.mpr h).isCoprime with ⟨a, b, hab⟩
[GOAL]
case mpr.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : a * ↑p + b * ↑(ringChar R) = 1
⊢ IsUnit ↑p
[PROOFSTEP]
apply_fun ((↑) : ℤ → R) at hab 
[GOAL]
case mpr.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : ↑(a * ↑p + b * ↑(ringChar R)) = ↑1
⊢ IsUnit ↑p
[PROOFSTEP]
push_cast at hab 
[GOAL]
case mpr.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : ↑a * ↑p + ↑b * ↑(ringChar R) = 1
⊢ IsUnit ↑p
[PROOFSTEP]
rw [hch, mul_zero, add_zero, mul_comm] at hab 
[GOAL]
case mpr.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : ↑p * ↑a = 1
⊢ IsUnit ↑p
[PROOFSTEP]
exact isUnit_of_mul_eq_one (p : R) a hab
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ p ∣ ringChar R ↔ p ∣ Fintype.card R
[PROOFSTEP]
refine'
  ⟨fun h =>
    h.trans <|
      Int.coe_nat_dvd.mp <|
        (CharP.int_cast_eq_zero_iff R (ringChar R) (Fintype.card R)).mp <| by exact_mod_cast CharP.cast_card_eq_zero R,
    fun h => _⟩
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ ringChar R
⊢ ↑↑(Fintype.card R) = 0
[PROOFSTEP]
exact_mod_cast CharP.cast_card_eq_zero R
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
⊢ p ∣ ringChar R
[PROOFSTEP]
by_contra h₀
[GOAL]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
⊢ False
[PROOFSTEP]
rcases exists_prime_addOrderOf_dvd_card p h with ⟨r, hr⟩
[GOAL]
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
⊢ False
[PROOFSTEP]
have hr₁ := addOrderOf_nsmul_eq_zero r
[GOAL]
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
hr₁ : addOrderOf r • r = 0
⊢ False
[PROOFSTEP]
rw [hr, nsmul_eq_mul] at hr₁ 
[GOAL]
case intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
hr₁ : ↑p * r = 0
⊢ False
[PROOFSTEP]
rcases IsUnit.exists_left_inv ((isUnit_iff_not_dvd_char R p).mpr h₀) with ⟨u, hu⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
hr₁ : ↑p * r = 0
u : R
hu : u * ↑p = 1
⊢ False
[PROOFSTEP]
apply_fun (· * ·) u at hr₁ 
[GOAL]
case intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
u : R
hu : u * ↑p = 1
hr₁ : u * (↑p * r) = u * 0
⊢ False
[PROOFSTEP]
rw [mul_zero, ← mul_assoc, hu, one_mul] at hr₁ 
[GOAL]
case intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
u : R
hu : u * ↑p = 1
hr₁ : r = 0
⊢ False
[PROOFSTEP]
exact mt AddMonoid.addOrderOf_eq_one_iff.mpr (ne_of_eq_of_ne hr (Nat.Prime.ne_one Fact.out)) hr₁
