K : Type ?u.1099307
R : Type ?u.1099310
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
h₁ : a ^ (Fintype.card F - 1) = 1
⊢ a ^ (Fintype.card F / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1
K : Type ?u.1099307
R : Type ?u.1099310
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ a ^ (Fintype.card F / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1
have h₁ := FiniteField.pow_card_sub_one_eq_one a ha
K : Type ?u.1099307
R : Type ?u.1099310
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
h₁ : a ^ (Fintype.card F / 2) * a ^ (Fintype.card F / 2) = 1
⊢ a ^ (Fintype.card F / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1
K : Type ?u.1099307
R : Type ?u.1099310
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
h₁ : a ^ (Fintype.card F - 1) = 1
⊢ a ^ (Fintype.card F / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1
rw [← Nat.two_mul_odd_div_two (FiniteField.odd_card_of_char_ne_two hF), mul_comm, pow_mul,
  pow_two] at h₁
no goals
K : Type ?u.1099307
R : Type ?u.1099310
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
h₁ : a ^ (Fintype.card F / 2) * a ^ (Fintype.card F / 2) = 1
⊢ a ^ (Fintype.card F / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1
exact mul_self_eq_one_iff.mp h₁