case intro
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : Fˣ
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := Fˣ)
case intro.intro
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hn : (fun x x_1 => x ^ x_1) g n = a
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
case intro
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
obtain ⟨n, hn⟩ : a ∈ Submonoid.powers g := by rw [mem_powers_iff_mem_zpowers]; apply hg
case intro.intro
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hn : (fun x x_1 => x ^ x_1) g n = a
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
case intro.intro
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hn : (fun x x_1 => x ^ x_1) g n = a
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
have hodd := Nat.two_mul_odd_div_two (FiniteField.odd_card_of_char_ne_two hF)
case intro.intro.mp
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hn : (fun x x_1 => x ^ x_1) g n = a
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
⊢ IsSquare a → a ^ (Fintype.card F / 2) = 1

case intro.intro.mpr
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hn : (fun x x_1 => x ^ x_1) g n = a
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
⊢ a ^ (Fintype.card F / 2) = 1 → IsSquare a
case intro.intro
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hn : (fun x x_1 => x ^ x_1) g n = a
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
constructor
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
⊢ a ∈ Subgroup.zpowers g
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
⊢ a ∈ Submonoid.powers g
rw [mem_powers_iff_mem_zpowers]
no goals
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
⊢ a ∈ Subgroup.zpowers g
apply hg
case intro.intro.mp.intro
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
y : Fˣ
hn : (fun x x_1 => x ^ x_1) g n = y * y
⊢ (y * y) ^ (Fintype.card F / 2) = 1
case intro.intro.mp
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hn : (fun x x_1 => x ^ x_1) g n = a
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
⊢ IsSquare a → a ^ (Fintype.card F / 2) = 1
rintro ⟨y, rfl⟩
case intro.intro.mp.intro
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
y : Fˣ
hn : (fun x x_1 => x ^ x_1) g n = y * y
⊢ y ^ (Fintype.card F - 1) = 1
case intro.intro.mp.intro
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
y : Fˣ
hn : (fun x x_1 => x ^ x_1) g n = y * y
⊢ (y * y) ^ (Fintype.card F / 2) = 1
rw [← pow_two, ← pow_mul, hodd]
case intro.intro.mp.intro
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
y : Fˣ
hn : (fun x x_1 => x ^ x_1) g n = y * y
⊢ ↑(y ^ (Fintype.card F - 1)) = ↑1
case intro.intro.mp.intro
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
y : Fˣ
hn : (fun x x_1 => x ^ x_1) g n = y * y
⊢ y ^ (Fintype.card F - 1) = 1
apply_fun Units.val using Units.ext (α := F)
case intro.intro.mp.intro
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
y : Fˣ
hn : (fun x x_1 => x ^ x_1) g n = y * y
⊢ ↑y ^ (Fintype.card F - 1) = 1
case intro.intro.mp.intro
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
y : Fˣ
hn : (fun x x_1 => x ^ x_1) g n = y * y
⊢ ↑(y ^ (Fintype.card F - 1)) = ↑1
push_cast
no goals
case intro.intro.mp.intro
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
y : Fˣ
hn : (fun x x_1 => x ^ x_1) g n = y * y
⊢ ↑y ^ (Fintype.card F - 1) = 1
exact FiniteField.pow_card_sub_one_eq_one (y : F) (Units.ne_zero y)
case intro.intro.mpr
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
⊢ (fun x x_1 => x ^ x_1) g n ^ (Fintype.card F / 2) = 1 → IsSquare ((fun x x_1 => x ^ x_1) g n)
case intro.intro.mpr
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hn : (fun x x_1 => x ^ x_1) g n = a
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
⊢ a ^ (Fintype.card F / 2) = 1 → IsSquare a
subst a
case intro.intro.mpr
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
h : (fun x x_1 => x ^ x_1) g n ^ (Fintype.card F / 2) = 1
⊢ IsSquare ((fun x x_1 => x ^ x_1) g n)
case intro.intro.mpr
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
⊢ (fun x x_1 => x ^ x_1) g n ^ (Fintype.card F / 2) = 1 → IsSquare ((fun x x_1 => x ^ x_1) g n)
intro h
case intro.intro.mpr
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
h : (fun x x_1 => x ^ x_1) g n ^ (Fintype.card F / 2) = 1
key : 2 * (Fintype.card F / 2) ∣ n * (Fintype.card F / 2)
⊢ IsSquare ((fun x x_1 => x ^ x_1) g n)
case intro.intro.mpr
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
h : (fun x x_1 => x ^ x_1) g n ^ (Fintype.card F / 2) = 1
⊢ IsSquare ((fun x x_1 => x ^ x_1) g n)
have key : 2 * (Fintype.card F / 2) ∣ n * (Fintype.card F / 2) := by
  rw [← pow_mul] at h
  rw [hodd, ← Fintype.card_units, ← orderOf_eq_card_of_forall_mem_zpowers hg]
  apply orderOf_dvd_of_pow_eq_one h
case intro.intro.mpr
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
h : (fun x x_1 => x ^ x_1) g n ^ (Fintype.card F / 2) = 1
key : 2 * (Fintype.card F / 2) ∣ n * (Fintype.card F / 2)
this : 0 < Fintype.card F / 2
⊢ IsSquare ((fun x x_1 => x ^ x_1) g n)
case intro.intro.mpr
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
h : (fun x x_1 => x ^ x_1) g n ^ (Fintype.card F / 2) = 1
key : 2 * (Fintype.card F / 2) ∣ n * (Fintype.card F / 2)
⊢ IsSquare ((fun x x_1 => x ^ x_1) g n)
have : 0 < Fintype.card F / 2 := Nat.div_pos Fintype.one_lt_card (by norm_num)
case intro.intro.mpr.intro
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
this : 0 < Fintype.card F / 2
m : ℕ
h : (fun x x_1 => x ^ x_1) g (2 * m) ^ (Fintype.card F / 2) = 1
key : 2 * (Fintype.card F / 2) ∣ 2 * m * (Fintype.card F / 2)
⊢ IsSquare ((fun x x_1 => x ^ x_1) g (2 * m))
case intro.intro.mpr
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
h : (fun x x_1 => x ^ x_1) g n ^ (Fintype.card F / 2) = 1
key : 2 * (Fintype.card F / 2) ∣ n * (Fintype.card F / 2)
this : 0 < Fintype.card F / 2
⊢ IsSquare ((fun x x_1 => x ^ x_1) g n)
obtain ⟨m, rfl⟩ := Nat.dvd_of_mul_dvd_mul_right this key
case intro.intro.mpr.intro
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
this : 0 < Fintype.card F / 2
m : ℕ
h : (fun x x_1 => x ^ x_1) g (2 * m) ^ (Fintype.card F / 2) = 1
key : 2 * (Fintype.card F / 2) ∣ 2 * m * (Fintype.card F / 2)
⊢ (fun x x_1 => x ^ x_1) g (2 * m) = g ^ m * g ^ m
case intro.intro.mpr.intro
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
this : 0 < Fintype.card F / 2
m : ℕ
h : (fun x x_1 => x ^ x_1) g (2 * m) ^ (Fintype.card F / 2) = 1
key : 2 * (Fintype.card F / 2) ∣ 2 * m * (Fintype.card F / 2)
⊢ IsSquare ((fun x x_1 => x ^ x_1) g (2 * m))
refine' ⟨g ^ m, _⟩
case intro.intro.mpr.intro
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
this : 0 < Fintype.card F / 2
m : ℕ
h : (fun x x_1 => x ^ x_1) g (2 * m) ^ (Fintype.card F / 2) = 1
key : 2 * (Fintype.card F / 2) ∣ 2 * m * (Fintype.card F / 2)
⊢ g ^ (2 * m) = g ^ m * g ^ m
case intro.intro.mpr.intro
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
this : 0 < Fintype.card F / 2
m : ℕ
h : (fun x x_1 => x ^ x_1) g (2 * m) ^ (Fintype.card F / 2) = 1
key : 2 * (Fintype.card F / 2) ∣ 2 * m * (Fintype.card F / 2)
⊢ (fun x x_1 => x ^ x_1) g (2 * m) = g ^ m * g ^ m
dsimp
no goals
case intro.intro.mpr.intro
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
this : 0 < Fintype.card F / 2
m : ℕ
h : (fun x x_1 => x ^ x_1) g (2 * m) ^ (Fintype.card F / 2) = 1
key : 2 * (Fintype.card F / 2) ∣ 2 * m * (Fintype.card F / 2)
⊢ g ^ (2 * m) = g ^ m * g ^ m
rw [mul_comm, pow_mul, pow_two]
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
h : g ^ (n * (Fintype.card F / 2)) = 1
⊢ 2 * (Fintype.card F / 2) ∣ n * (Fintype.card F / 2)
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
h : (fun x x_1 => x ^ x_1) g n ^ (Fintype.card F / 2) = 1
⊢ 2 * (Fintype.card F / 2) ∣ n * (Fintype.card F / 2)
rw [← pow_mul] at h
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
h : g ^ (n * (Fintype.card F / 2)) = 1
⊢ orderOf g ∣ n * (Fintype.card F / 2)
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
h : g ^ (n * (Fintype.card F / 2)) = 1
⊢ 2 * (Fintype.card F / 2) ∣ n * (Fintype.card F / 2)
rw [hodd, ← Fintype.card_units, ← orderOf_eq_card_of_forall_mem_zpowers hg]
no goals
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
h : g ^ (n * (Fintype.card F / 2)) = 1
⊢ orderOf g ∣ n * (Fintype.card F / 2)
apply orderOf_dvd_of_pow_eq_one h
no goals
K : Type ?u.1100843
R : Type ?u.1100846
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
h : (fun x x_1 => x ^ x_1) g n ^ (Fintype.card F / 2) = 1
key : 2 * (Fintype.card F / 2) ∣ n * (Fintype.card F / 2)
⊢ 0 < 2
norm_num