case intro.intro
K : Type ?u.1097070
R : Type ?u.1097073
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
⊢ ringChar F = 2 ↔ Fintype.card F % 2 = 0
K : Type ?u.1097070
R : Type ?u.1097073
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
⊢ ringChar F = 2 ↔ Fintype.card F % 2 = 0
rcases FiniteField.card F (ringChar F) with ⟨n, hp, h⟩
case intro.intro
K : Type ?u.1097070
R : Type ?u.1097073
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
⊢ ringChar F = 2 ↔ (ringChar F % 2) ^ ↑n % 2 = 0
case intro.intro
K : Type ?u.1097070
R : Type ?u.1097073
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
⊢ ringChar F = 2 ↔ Fintype.card F % 2 = 0
rw [h, Nat.pow_mod]
case intro.intro.mp
K : Type ?u.1097070
R : Type ?u.1097073
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
⊢ ringChar F = 2 → (ringChar F % 2) ^ ↑n % 2 = 0

case intro.intro.mpr
K : Type ?u.1097070
R : Type ?u.1097073
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
⊢ (ringChar F % 2) ^ ↑n % 2 = 0 → ringChar F = 2
case intro.intro
K : Type ?u.1097070
R : Type ?u.1097073
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
⊢ ringChar F = 2 ↔ (ringChar F % 2) ^ ↑n % 2 = 0
constructor
case intro.intro.mp
K : Type ?u.1097070
R : Type ?u.1097073
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
hF : ringChar F = 2
⊢ (ringChar F % 2) ^ ↑n % 2 = 0
case intro.intro.mp
K : Type ?u.1097070
R : Type ?u.1097073
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
⊢ ringChar F = 2 → (ringChar F % 2) ^ ↑n % 2 = 0
intro hF
no goals
case intro.intro.mp
K : Type ?u.1097070
R : Type ?u.1097073
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
hF : ringChar F = 2
⊢ (ringChar F % 2) ^ ↑n % 2 = 0
simp [hF]
case intro.intro.mpr
K : Type ?u.1097070
R : Type ?u.1097073
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
⊢ Even (ringChar F % 2) ∧ ↑n ≠ 0 → ringChar F = 2
case intro.intro.mpr
K : Type ?u.1097070
R : Type ?u.1097073
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
⊢ (ringChar F % 2) ^ ↑n % 2 = 0 → ringChar F = 2
rw [← Nat.even_iff, Nat.even_pow]
case intro.intro.mpr.intro
K : Type ?u.1097070
R : Type ?u.1097073
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
hev : Even (ringChar F % 2)
hnz : ↑n ≠ 0
⊢ ringChar F = 2
case intro.intro.mpr
K : Type ?u.1097070
R : Type ?u.1097073
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
⊢ Even (ringChar F % 2) ∧ ↑n ≠ 0 → ringChar F = 2
rintro ⟨hev, hnz⟩
case intro.intro.mpr.intro
K : Type ?u.1097070
R : Type ?u.1097073
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
hev : ringChar F % 2 = 0
hnz : ↑n ≠ 0
⊢ ringChar F = 2
case intro.intro.mpr.intro
K : Type ?u.1097070
R : Type ?u.1097073
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
hev : Even (ringChar F % 2)
hnz : ↑n ≠ 0
⊢ ringChar F = 2
rw [Nat.even_iff, Nat.mod_mod] at hev
no goals
case intro.intro.mpr.intro
K : Type ?u.1097070
R : Type ?u.1097073
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
hev : ringChar F % 2 = 0
hnz : ↑n ≠ 0
⊢ ringChar F = 2
exact (Nat.Prime.eq_two_or_odd hp).resolve_right (ne_of_eq_of_ne hev zero_ne_one)