K : Type u_1
R : Type ?u.399990
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n
K : Type u_1
R : Type ?u.399990
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n
haveI hp : Fact p.Prime := ⟨CharP.char_is_prime K p⟩
K : Type u_1
R : Type ?u.399990
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let src := RingHom.toModule (ZMod.castHom (_ : p ∣ p) K);
  Module.mk (_ : ∀ (r s : ZMod p) (x : K), (r + s) • x = r • x + s • x) (_ : ∀ (x : K), 0 • x = 0)
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n
K : Type u_1
R : Type ?u.399990
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n
letI : Module (ZMod p) K := { (ZMod.castHom dvd_rfl K : ZMod p →+* _).toModule with }
case intro
K : Type u_1
R : Type ?u.399990
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let src := RingHom.toModule (ZMod.castHom (_ : p ∣ p) K);
  Module.mk (_ : ∀ (r s : ZMod p) (x : K), (r + s) • x = r • x + s • x) (_ : ∀ (x : K), 0 • x = 0)
n : ℕ
h : q = Fintype.card (ZMod p) ^ n
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n
K : Type u_1
R : Type ?u.399990
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let src := RingHom.toModule (ZMod.castHom (_ : p ∣ p) K);
  Module.mk (_ : ∀ (r s : ZMod p) (x : K), (r + s) • x = r • x + s • x) (_ : ∀ (x : K), 0 • x = 0)
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n
obtain ⟨n, h⟩ := VectorSpace.card_fintype (ZMod p) K
case intro
K : Type u_1
R : Type ?u.399990
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let src := RingHom.toModule (ZMod.castHom (_ : p ∣ p) K);
  Module.mk (_ : ∀ (r s : ZMod p) (x : K), (r + s) • x = r • x + s • x) (_ : ∀ (x : K), 0 • x = 0)
n : ℕ
h : q = p ^ n
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n
case intro
K : Type u_1
R : Type ?u.399990
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let src := RingHom.toModule (ZMod.castHom (_ : p ∣ p) K);
  Module.mk (_ : ∀ (r s : ZMod p) (x : K), (r + s) • x = r • x + s • x) (_ : ∀ (x : K), 0 • x = 0)
n : ℕ
h : q = Fintype.card (ZMod p) ^ n
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n
rw [ZMod.card] at h
case intro
K : Type u_1
R : Type ?u.399990
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let src := RingHom.toModule (ZMod.castHom (_ : p ∣ p) K);
  Module.mk (_ : ∀ (r s : ZMod p) (x : K), (r + s) • x = r • x + s • x) (_ : ∀ (x : K), 0 • x = 0)
n : ℕ
h : q = p ^ n
⊢ 0 < n
case intro
K : Type u_1
R : Type ?u.399990
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let src := RingHom.toModule (ZMod.castHom (_ : p ∣ p) K);
  Module.mk (_ : ∀ (r s : ZMod p) (x : K), (r + s) • x = r • x + s • x) (_ : ∀ (x : K), 0 • x = 0)
n : ℕ
h : q = p ^ n
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n
refine' ⟨⟨n, _⟩, hp.1, h⟩
case intro
K : Type u_1
R : Type ?u.399990
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let src := RingHom.toModule (ZMod.castHom (_ : p ∣ p) K);
  Module.mk (_ : ∀ (r s : ZMod p) (x : K), (r + s) • x = r • x + s • x) (_ : ∀ (x : K), 0 • x = 0)
n : ℕ
h : q = p ^ n
⊢ ¬n = 0
case intro
K : Type u_1
R : Type ?u.399990
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let src := RingHom.toModule (ZMod.castHom (_ : p ∣ p) K);
  Module.mk (_ : ∀ (r s : ZMod p) (x : K), (r + s) • x = r • x + s • x) (_ : ∀ (x : K), 0 • x = 0)
n : ℕ
h : q = p ^ n
⊢ 0 < n
apply Or.resolve_left (Nat.eq_zero_or_pos n)
case intro
K : Type u_1
R : Type ?u.399990
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let src := RingHom.toModule (ZMod.castHom (_ : p ∣ p) K);
  Module.mk (_ : ∀ (r s : ZMod p) (x : K), (r + s) • x = r • x + s • x) (_ : ∀ (x : K), 0 • x = 0)
h : q = p ^ 0
⊢ False
case intro
K : Type u_1
R : Type ?u.399990
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let src := RingHom.toModule (ZMod.castHom (_ : p ∣ p) K);
  Module.mk (_ : ∀ (r s : ZMod p) (x : K), (r + s) • x = r • x + s • x) (_ : ∀ (x : K), 0 • x = 0)
n : ℕ
h : q = p ^ n
⊢ ¬n = 0
rintro rfl
case intro
K : Type u_1
R : Type ?u.399990
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let src := RingHom.toModule (ZMod.castHom (_ : p ∣ p) K);
  Module.mk (_ : ∀ (r s : ZMod p) (x : K), (r + s) • x = r • x + s • x) (_ : ∀ (x : K), 0 • x = 0)
h : q = 1
⊢ False
case intro
K : Type u_1
R : Type ?u.399990
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let src := RingHom.toModule (ZMod.castHom (_ : p ∣ p) K);
  Module.mk (_ : ∀ (r s : ZMod p) (x : K), (r + s) • x = r • x + s • x) (_ : ∀ (x : K), 0 • x = 0)
h : q = p ^ 0
⊢ False
rw [pow_zero] at h
case intro
K : Type u_1
R : Type ?u.399990
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this✝ : Module (ZMod p) K :=
  let src := RingHom.toModule (ZMod.castHom (_ : p ∣ p) K);
  Module.mk (_ : ∀ (r s : ZMod p) (x : K), (r + s) • x = r • x + s • x) (_ : ∀ (x : K), 0 • x = 0)
h : q = 1
this : 0 = 1
⊢ False
case intro
K : Type u_1
R : Type ?u.399990
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let src := RingHom.toModule (ZMod.castHom (_ : p ∣ p) K);
  Module.mk (_ : ∀ (r s : ZMod p) (x : K), (r + s) • x = r • x + s • x) (_ : ∀ (x : K), 0 • x = 0)
h : q = 1
⊢ False
have : (0 : K) = 1 := by apply Fintype.card_le_one_iff.mp (le_of_eq h)
no goals
case intro
K : Type u_1
R : Type ?u.399990
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this✝ : Module (ZMod p) K :=
  let src := RingHom.toModule (ZMod.castHom (_ : p ∣ p) K);
  Module.mk (_ : ∀ (r s : ZMod p) (x : K), (r + s) • x = r • x + s • x) (_ : ∀ (x : K), 0 • x = 0)
h : q = 1
this : 0 = 1
⊢ False
exact absurd this zero_ne_one
no goals
K : Type u_1
R : Type ?u.399990
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let src := RingHom.toModule (ZMod.castHom (_ : p ∣ p) K);
  Module.mk (_ : ∀ (r s : ZMod p) (x : K), (r + s) • x = r • x + s • x) (_ : ∀ (x : K), 0 • x = 0)
h : q = 1
⊢ 0 = 1
apply Fintype.card_le_one_iff.mp (le_of_eq h)