[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
⊢ quadraticCharFun F a = 0 ↔ a = 0
[PROOFSTEP]
simp only [quadraticCharFun]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
⊢ (if a = 0 then 0 else if IsSquare a then 1 else -1) = 0 ↔ a = 0
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a = 0
⊢ (if a = 0 then 0 else if IsSquare a then 1 else -1) = 0 ↔ a = 0
[PROOFSTEP]
simp only [ha, eq_self_iff_true, if_true]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
⊢ (if a = 0 then 0 else if IsSquare a then 1 else -1) = 0 ↔ a = 0
[PROOFSTEP]
simp only [ha, if_false, iff_false_iff]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
⊢ ¬(if IsSquare a then 1 else -1) = 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
h✝ : IsSquare a
⊢ ¬1 = 0
[PROOFSTEP]
simp only [neg_eq_zero, one_ne_zero, not_false_iff]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
h✝ : ¬IsSquare a
⊢ ¬-1 = 0
[PROOFSTEP]
simp only [neg_eq_zero, one_ne_zero, not_false_iff]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
⊢ quadraticCharFun F 0 = 0
[PROOFSTEP]
simp only [quadraticCharFun, eq_self_iff_true, if_true, id.def]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
⊢ quadraticCharFun F 1 = 1
[PROOFSTEP]
simp only [quadraticCharFun, one_ne_zero, isSquare_one, if_true, if_false, id.def]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F = 2
a : F
ha : a ≠ 0
⊢ quadraticCharFun F a = 1
[PROOFSTEP]
simp only [quadraticCharFun, ha, if_false, ite_eq_left_iff]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F = 2
a : F
ha : a ≠ 0
⊢ ¬IsSquare a → False
[PROOFSTEP]
exact fun h => h (FiniteField.isSquare_of_char_two hF a)
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ quadraticCharFun F a = if a ^ (Fintype.card F / 2) = 1 then 1 else -1
[PROOFSTEP]
simp only [quadraticCharFun, ha, if_false]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ (if IsSquare a then 1 else -1) = if a ^ (Fintype.card F / 2) = 1 then 1 else -1
[PROOFSTEP]
simp_rw [FiniteField.isSquare_iff hF ha]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : a = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
[PROOFSTEP]
rw [ha, zero_mul, quadraticCharFun_zero, zero_mul]
  -- now `a ≠ 0`
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
[PROOFSTEP]
by_cases hb : b = 0
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : b = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
[PROOFSTEP]
rw [hb, mul_zero, quadraticCharFun_zero, mul_zero]
  -- now `a ≠ 0` and `b ≠ 0`
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
[PROOFSTEP]
have hab := mul_ne_zero ha hb
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
[PROOFSTEP]
by_cases hF : ringChar F = 2
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ringChar F = 2
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
[PROOFSTEP]
rw [quadraticCharFun_eq_one_of_char_two hF ha, quadraticCharFun_eq_one_of_char_two hF hb,
  quadraticCharFun_eq_one_of_char_two hF hab, mul_one]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
[PROOFSTEP]
rw [quadraticCharFun_eq_pow_of_char_ne_two hF ha, quadraticCharFun_eq_pow_of_char_ne_two hF hb,
  quadraticCharFun_eq_pow_of_char_ne_two hF hab, mul_pow]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
⊢ (if a ^ (Fintype.card F / 2) * b ^ (Fintype.card F / 2) = 1 then 1 else -1) =
    (if a ^ (Fintype.card F / 2) = 1 then 1 else -1) * if b ^ (Fintype.card F / 2) = 1 then 1 else -1
[PROOFSTEP]
cases' FiniteField.pow_dichotomy hF hb with hb' hb'
[GOAL]
case neg.inl
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
hb' : b ^ (Fintype.card F / 2) = 1
⊢ (if a ^ (Fintype.card F / 2) * b ^ (Fintype.card F / 2) = 1 then 1 else -1) =
    (if a ^ (Fintype.card F / 2) = 1 then 1 else -1) * if b ^ (Fintype.card F / 2) = 1 then 1 else -1
[PROOFSTEP]
simp only [hb', mul_one, eq_self_iff_true, if_true]
[GOAL]
case neg.inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
hb' : b ^ (Fintype.card F / 2) = -1
⊢ (if a ^ (Fintype.card F / 2) * b ^ (Fintype.card F / 2) = 1 then 1 else -1) =
    (if a ^ (Fintype.card F / 2) = 1 then 1 else -1) * if b ^ (Fintype.card F / 2) = 1 then 1 else -1
[PROOFSTEP]
have h := Ring.neg_one_ne_one_of_char_ne_two hF
[GOAL]
case neg.inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
hb' : b ^ (Fintype.card F / 2) = -1
h : -1 ≠ 1
⊢ (if a ^ (Fintype.card F / 2) * b ^ (Fintype.card F / 2) = 1 then 1 else -1) =
    (if a ^ (Fintype.card F / 2) = 1 then 1 else -1) * if b ^ (Fintype.card F / 2) = 1 then 1 else -1
[PROOFSTEP]
simp only [hb', h, mul_neg, mul_one, if_false, ite_mul, neg_mul]
[GOAL]
case neg.inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
hb' : b ^ (Fintype.card F / 2) = -1
h : -1 ≠ 1
⊢ (if -a ^ (Fintype.card F / 2) = 1 then 1 else -1) = -if a ^ (Fintype.card F / 2) = 1 then 1 else -1
[PROOFSTEP]
cases' FiniteField.pow_dichotomy hF ha with ha' ha'
[GOAL]
case neg.inr.inl
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
hb' : b ^ (Fintype.card F / 2) = -1
h : -1 ≠ 1
ha' : a ^ (Fintype.card F / 2) = 1
⊢ (if -a ^ (Fintype.card F / 2) = 1 then 1 else -1) = -if a ^ (Fintype.card F / 2) = 1 then 1 else -1
[PROOFSTEP]
simp only [ha', h, neg_neg, eq_self_iff_true, if_true, if_false]
[GOAL]
case neg.inr.inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
hb' : b ^ (Fintype.card F / 2) = -1
h : -1 ≠ 1
ha' : a ^ (Fintype.card F / 2) = -1
⊢ (if -a ^ (Fintype.card F / 2) = 1 then 1 else -1) = -if a ^ (Fintype.card F / 2) = 1 then 1 else -1
[PROOFSTEP]
simp only [ha', h, neg_neg, eq_self_iff_true, if_true, if_false]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬IsUnit a
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := quadraticCharFun F, map_one' := (_ : quadraticCharFun F 1 = 1) },
          map_mul' := (_ : ∀ (a b : F), quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b) })
      a =
    0
[PROOFSTEP]
rw [of_not_not (mt Ne.isUnit ha)]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬IsUnit a
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := quadraticCharFun F, map_one' := (_ : quadraticCharFun F 1 = 1) },
          map_mul' := (_ : ∀ (a b : F), quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b) })
      0 =
    0
[PROOFSTEP]
exact quadraticCharFun_zero
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
⊢ ↑(quadraticChar F) 0 = 0
[PROOFSTEP]
simp only [quadraticChar_apply, quadraticCharFun_zero]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
⊢ ↑(quadraticChar F) a = 1 ↔ IsSquare a
[PROOFSTEP]
simp only [quadraticChar_apply, quadraticCharFun, ha, (by decide : (-1 : ℤ) ≠ 1), if_false, ite_eq_left_iff, imp_false,
  Classical.not_not]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
⊢ -1 ≠ 1
[PROOFSTEP]
decide
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
⊢ ↑(quadraticChar F) (a ^ 2) = 1
[PROOFSTEP]
simp only [quadraticCharFun, ha, pow_eq_zero_iff, Nat.succ_pos', IsSquare_sq, if_true, if_false, quadraticChar_apply]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
⊢ ↑(quadraticChar F) a ^ 2 = 1
[PROOFSTEP]
erw [pow_two, ← map_mul (quadraticChar F) a, ← pow_two]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
⊢ ↑(quadraticChar F) (a ^ 2) = 1
[PROOFSTEP]
apply quadraticChar_sq_one' ha
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
⊢ ↑(quadraticChar F) a = -1 ↔ ¬↑(quadraticChar F) a = 1
[PROOFSTEP]
refine' ⟨fun h => _, fun h₂ => (or_iff_right h₂).mp (quadraticChar_dichotomy ha)⟩
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
h : ↑(quadraticChar F) a = -1
⊢ ¬↑(quadraticChar F) a = 1
[PROOFSTEP]
rw [h]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
h : ↑(quadraticChar F) a = -1
⊢ ¬-1 = 1
[PROOFSTEP]
norm_num
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
⊢ ↑(quadraticChar F) a = -1 ↔ ¬IsSquare a
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a = 0
⊢ ↑(quadraticChar F) a = -1 ↔ ¬IsSquare a
[PROOFSTEP]
simp only [ha, isSquare_zero, MulChar.map_zero, zero_eq_neg, one_ne_zero, not_true]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
⊢ ↑(quadraticChar F) a = -1 ↔ ¬IsSquare a
[PROOFSTEP]
rw [quadraticChar_eq_neg_one_iff_not_one ha, quadraticChar_one_iff_isSquare ha]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
⊢ ↑(↑(quadraticChar F) a) = a ^ (Fintype.card F / 2)
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : a = 0
⊢ ↑(↑(quadraticChar F) a) = a ^ (Fintype.card F / 2)
[PROOFSTEP]
have : 0 < Fintype.card F / 2 := Nat.div_pos Fintype.one_lt_card two_pos
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : a = 0
this : 0 < Fintype.card F / 2
⊢ ↑(↑(quadraticChar F) a) = a ^ (Fintype.card F / 2)
[PROOFSTEP]
simp only [ha, zero_pow this, quadraticChar_apply, quadraticCharFun_zero, Int.cast_zero]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ¬a = 0
⊢ ↑(↑(quadraticChar F) a) = a ^ (Fintype.card F / 2)
[PROOFSTEP]
rw [quadraticChar_eq_pow_of_char_ne_two hF ha]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ¬a = 0
⊢ ↑(if a ^ (Fintype.card F / 2) = 1 then 1 else -1) = a ^ (Fintype.card F / 2)
[PROOFSTEP]
by_cases ha' : a ^ (Fintype.card F / 2) = 1
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ¬a = 0
ha' : a ^ (Fintype.card F / 2) = 1
⊢ ↑(if a ^ (Fintype.card F / 2) = 1 then 1 else -1) = a ^ (Fintype.card F / 2)
[PROOFSTEP]
simp only [ha', eq_self_iff_true, if_true, Int.cast_one]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ¬a = 0
ha' : ¬a ^ (Fintype.card F / 2) = 1
⊢ ↑(if a ^ (Fintype.card F / 2) = 1 then 1 else -1) = a ^ (Fintype.card F / 2)
[PROOFSTEP]
have ha'' := Or.resolve_left (FiniteField.pow_dichotomy hF ha) ha'
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ¬a = 0
ha' : ¬a ^ (Fintype.card F / 2) = 1
ha'' : a ^ (Fintype.card F / 2) = -1
⊢ ↑(if a ^ (Fintype.card F / 2) = 1 then 1 else -1) = a ^ (Fintype.card F / 2)
[PROOFSTEP]
simp only [ha'', Int.cast_ite, Int.cast_one, Int.cast_neg, ite_eq_right_iff]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ¬a = 0
ha' : ¬a ^ (Fintype.card F / 2) = 1
ha'' : a ^ (Fintype.card F / 2) = -1
⊢ -1 = 1 → 1 = -1
[PROOFSTEP]
exact Eq.symm
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
⊢ IsQuadratic (quadraticChar F)
[PROOFSTEP]
intro a
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
⊢ ↑(quadraticChar F) a = 0 ∨ ↑(quadraticChar F) a = 1 ∨ ↑(quadraticChar F) a = -1
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a = 0
⊢ ↑(quadraticChar F) a = 0 ∨ ↑(quadraticChar F) a = 1 ∨ ↑(quadraticChar F) a = -1
[PROOFSTEP]
left
[GOAL]
case pos.h
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a = 0
⊢ ↑(quadraticChar F) a = 0
[PROOFSTEP]
rw [ha]
[GOAL]
case pos.h
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a = 0
⊢ ↑(quadraticChar F) 0 = 0
[PROOFSTEP]
exact quadraticChar_zero
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
⊢ ↑(quadraticChar F) a = 0 ∨ ↑(quadraticChar F) a = 1 ∨ ↑(quadraticChar F) a = -1
[PROOFSTEP]
right
[GOAL]
case neg.h
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
⊢ ↑(quadraticChar F) a = 1 ∨ ↑(quadraticChar F) a = -1
[PROOFSTEP]
exact quadraticChar_dichotomy ha
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ IsNontrivial (quadraticChar F)
[PROOFSTEP]
rcases quadraticChar_exists_neg_one hF with ⟨a, ha⟩
[GOAL]
case intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ↑(quadraticChar F) a = -1
⊢ IsNontrivial (quadraticChar F)
[PROOFSTEP]
have hu : IsUnit a := by by_contra hf; rw [MulChar.map_nonunit _ hf] at ha ; norm_num at ha 
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ↑(quadraticChar F) a = -1
⊢ IsUnit a
[PROOFSTEP]
by_contra hf
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ↑(quadraticChar F) a = -1
hf : ¬IsUnit a
⊢ False
[PROOFSTEP]
rw [MulChar.map_nonunit _ hf] at ha 
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : 0 = -1
hf : ¬IsUnit a
⊢ False
[PROOFSTEP]
norm_num at ha 
[GOAL]
case intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ↑(quadraticChar F) a = -1
hu : IsUnit a
⊢ IsNontrivial (quadraticChar F)
[PROOFSTEP]
refine' ⟨hu.unit, (_ : quadraticChar F a ≠ 1)⟩
[GOAL]
case intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ↑(quadraticChar F) a = -1
hu : IsUnit a
⊢ ↑(quadraticChar F) a ≠ 1
[PROOFSTEP]
rw [ha]
[GOAL]
case intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ↑(quadraticChar F) a = -1
hu : IsUnit a
⊢ -1 ≠ 1
[PROOFSTEP]
norm_num
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
⊢ ↑(Finset.card (Set.toFinset {x | x ^ 2 = a})) = ↑(quadraticChar F) a + 1
[PROOFSTEP]
by_cases h₀ : a = 0
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : a = 0
⊢ ↑(Finset.card (Set.toFinset {x | x ^ 2 = a})) = ↑(quadraticChar F) a + 1
[PROOFSTEP]
simp only [h₀, pow_eq_zero_iff, Nat.succ_pos', Int.ofNat_succ, Int.ofNat_zero, MulChar.map_zero,
  Set.setOf_eq_eq_singleton, Set.toFinset_card, Set.card_singleton]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
⊢ ↑(Finset.card (Set.toFinset {x | x ^ 2 = a})) = ↑(quadraticChar F) a + 1
[PROOFSTEP]
set s := {x : F | x ^ 2 = a}.toFinset
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := Set.toFinset {x | x ^ 2 = a}
⊢ ↑(Finset.card s) = ↑(quadraticChar F) a + 1
[PROOFSTEP]
by_cases h : IsSquare a
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := Set.toFinset {x | x ^ 2 = a}
h : IsSquare a
⊢ ↑(Finset.card s) = ↑(quadraticChar F) a + 1
[PROOFSTEP]
rw [(quadraticChar_one_iff_isSquare h₀).mpr h]
[GOAL]
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := Set.toFinset {x | x ^ 2 = a}
h : IsSquare a
⊢ ↑(Finset.card s) = 1 + 1
[PROOFSTEP]
rcases h with ⟨b, h⟩
[GOAL]
case pos.intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h : a = b * b
⊢ ↑(Finset.card s) = 1 + 1
[PROOFSTEP]
rw [h, mul_self_eq_zero] at h₀ 
[GOAL]
case pos.intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b * b
⊢ ↑(Finset.card s) = 1 + 1
[PROOFSTEP]
have h₁ : s = [b, -b].toFinset := by
  ext x
  simp only [Finset.mem_filter, Finset.mem_univ, true_and_iff, List.toFinset_cons, List.toFinset_nil, insert_emptyc_eq,
    Finset.mem_insert, Finset.mem_singleton]
  rw [← pow_two] at h 
  simp only [h, Set.toFinset_setOf, Finset.mem_univ, Finset.mem_filter, true_and]
  constructor
  · exact eq_or_eq_neg_of_sq_eq_sq _ _
  · rintro (h₂ | h₂) <;> rw [h₂]
    simp only [neg_sq]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b * b
⊢ s = List.toFinset [b, -b]
[PROOFSTEP]
ext x
[GOAL]
case a
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b * b
x : F
⊢ x ∈ s ↔ x ∈ List.toFinset [b, -b]
[PROOFSTEP]
simp only [Finset.mem_filter, Finset.mem_univ, true_and_iff, List.toFinset_cons, List.toFinset_nil, insert_emptyc_eq,
  Finset.mem_insert, Finset.mem_singleton]
[GOAL]
case a
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b * b
x : F
⊢ x ∈ Set.toFinset {x | x ^ 2 = a} ↔ x = b ∨ x = -b
[PROOFSTEP]
rw [← pow_two] at h 
[GOAL]
case a
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b ^ 2
x : F
⊢ x ∈ Set.toFinset {x | x ^ 2 = a} ↔ x = b ∨ x = -b
[PROOFSTEP]
simp only [h, Set.toFinset_setOf, Finset.mem_univ, Finset.mem_filter, true_and]
[GOAL]
case a
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b ^ 2
x : F
⊢ x ^ 2 = b ^ 2 ↔ x = b ∨ x = -b
[PROOFSTEP]
constructor
[GOAL]
case a.mp
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b ^ 2
x : F
⊢ x ^ 2 = b ^ 2 → x = b ∨ x = -b
[PROOFSTEP]
exact eq_or_eq_neg_of_sq_eq_sq _ _
[GOAL]
case a.mpr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b ^ 2
x : F
⊢ x = b ∨ x = -b → x ^ 2 = b ^ 2
[PROOFSTEP]
rintro (h₂ | h₂)
[GOAL]
case a.mpr.inl
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b ^ 2
x : F
h₂ : x = b
⊢ x ^ 2 = b ^ 2
[PROOFSTEP]
rw [h₂]
[GOAL]
case a.mpr.inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b ^ 2
x : F
h₂ : x = -b
⊢ x ^ 2 = b ^ 2
[PROOFSTEP]
rw [h₂]
[GOAL]
case a.mpr.inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b ^ 2
x : F
h₂ : x = -b
⊢ (-b) ^ 2 = b ^ 2
[PROOFSTEP]
simp only [neg_sq]
[GOAL]
case pos.intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b * b
h₁ : s = List.toFinset [b, -b]
⊢ ↑(Finset.card s) = 1 + 1
[PROOFSTEP]
norm_cast
[GOAL]
case pos.intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b * b
h₁ : s = List.toFinset [b, -b]
⊢ Finset.card s = 1 + 1
[PROOFSTEP]
rw [h₁, List.toFinset_cons, List.toFinset_cons, List.toFinset_nil]
[GOAL]
case pos.intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := Set.toFinset {x | x ^ 2 = a}
b : F
h₀ : ¬b = 0
h : a = b * b
h₁ : s = List.toFinset [b, -b]
⊢ Finset.card (insert b (insert (-b) ∅)) = 1 + 1
[PROOFSTEP]
exact Finset.card_doubleton (Ne.symm (mt (Ring.eq_self_iff_eq_zero_of_char_ne_two hF).mp h₀))
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := Set.toFinset {x | x ^ 2 = a}
h : ¬IsSquare a
⊢ ↑(Finset.card s) = ↑(quadraticChar F) a + 1
[PROOFSTEP]
rw [quadraticChar_neg_one_iff_not_isSquare.mpr h]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := Set.toFinset {x | x ^ 2 = a}
h : ¬IsSquare a
⊢ ↑(Finset.card s) = -1 + 1
[PROOFSTEP]
simp only [Int.coe_nat_eq_zero, Finset.card_eq_zero, Set.toFinset_card, Fintype.card_ofFinset, Set.mem_setOf_eq,
  add_left_neg]
[GOAL]
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := Set.toFinset {x | x ^ 2 = a}
h : ¬IsSquare a
⊢ Set.toFinset {x | x ^ 2 = a} = ∅
[PROOFSTEP]
ext x
[GOAL]
case neg.a
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := Set.toFinset {x | x ^ 2 = a}
h : ¬IsSquare a
x : F
⊢ x ∈ Set.toFinset {x | x ^ 2 = a} ↔ x ∈ ∅
[PROOFSTEP]
simp only [iff_false_iff, Finset.mem_filter, Finset.mem_univ, true_and_iff, Finset.not_mem_empty, (Set.mem_toFinset),
  Set.mem_setOf]
[GOAL]
case neg.a
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := Set.toFinset {x | x ^ 2 = a}
h : ¬IsSquare a
x : F
⊢ ¬x ^ 2 = a
[PROOFSTEP]
rw [isSquare_iff_exists_sq] at h 
[GOAL]
case neg.a
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := Set.toFinset {x | x ^ 2 = a}
h : ¬∃ c, a = c ^ 2
x : F
⊢ ¬x ^ 2 = a
[PROOFSTEP]
exact fun h' => h ⟨_, h'.symm⟩
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ ↑(quadraticChar F) (-1) = ↑χ₄ ↑(Fintype.card F)
[PROOFSTEP]
have h := quadraticChar_eq_pow_of_char_ne_two hF (neg_ne_zero.mpr one_ne_zero)
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
h : ↑(quadraticChar F) (-1) = if (-1) ^ (Fintype.card F / 2) = 1 then 1 else -1
⊢ ↑(quadraticChar F) (-1) = ↑χ₄ ↑(Fintype.card F)
[PROOFSTEP]
rw [h, χ₄_eq_neg_one_pow (FiniteField.odd_card_of_char_ne_two hF)]
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
h : ↑(quadraticChar F) (-1) = if (-1) ^ (Fintype.card F / 2) = 1 then 1 else -1
⊢ (if (-1) ^ (Fintype.card F / 2) = 1 then 1 else -1) = (-1) ^ (Fintype.card F / 2)
[PROOFSTEP]
set n := Fintype.card F / 2
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
n : ℕ := Fintype.card F / 2
h : ↑(quadraticChar F) (-1) = if (-1) ^ n = 1 then 1 else -1
⊢ (if (-1) ^ n = 1 then 1 else -1) = (-1) ^ n
[PROOFSTEP]
cases' Nat.even_or_odd n with h₂ h₂
[GOAL]
case inl
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
n : ℕ := Fintype.card F / 2
h : ↑(quadraticChar F) (-1) = if (-1) ^ n = 1 then 1 else -1
h₂ : Even n
⊢ (if (-1) ^ n = 1 then 1 else -1) = (-1) ^ n
[PROOFSTEP]
simp only [Even.neg_one_pow h₂, eq_self_iff_true, if_true]
[GOAL]
case inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
n : ℕ := Fintype.card F / 2
h : ↑(quadraticChar F) (-1) = if (-1) ^ n = 1 then 1 else -1
h₂ : Odd n
⊢ (if (-1) ^ n = 1 then 1 else -1) = (-1) ^ n
[PROOFSTEP]
simp only [Odd.neg_one_pow h₂, Ring.neg_one_ne_one_of_char_ne_two hF, ite_false]
[GOAL]
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
⊢ IsSquare (-1) ↔ Fintype.card F % 4 ≠ 3
[PROOFSTEP]
classical
  -- suggested by the linter (instead of `[DecidableEq F]`)
by_cases hF : ringChar F = 2
· simp only [FiniteField.isSquare_of_char_two hF, Ne.def, true_iff_iff]
  exact fun hf => one_ne_zero <| (Nat.odd_of_mod_four_eq_three hf).symm.trans <| FiniteField.even_card_of_char_two hF
· have h₁ := FiniteField.odd_card_of_char_ne_two hF
  rw [← quadraticChar_one_iff_isSquare (neg_ne_zero.mpr (one_ne_zero' F)), quadraticChar_neg_one hF,
    χ₄_nat_eq_if_mod_four, h₁]
  simp only [Nat.one_ne_zero, if_false, ite_eq_left_iff, Ne.def, (by decide : (-1 : ℤ) ≠ 1), imp_false,
    Classical.not_not]
  exact ⟨fun h => ne_of_eq_of_ne h (by decide : 1 ≠ 3), Or.resolve_right (Nat.odd_mod_four_iff.mp h₁)⟩
[GOAL]
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
⊢ IsSquare (-1) ↔ Fintype.card F % 4 ≠ 3
[PROOFSTEP]
by_cases hF : ringChar F = 2
[GOAL]
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
⊢ IsSquare (-1) ↔ Fintype.card F % 4 ≠ 3
[PROOFSTEP]
simp only [FiniteField.isSquare_of_char_two hF, Ne.def, true_iff_iff]
[GOAL]
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
⊢ ¬Fintype.card F % 4 = 3
[PROOFSTEP]
exact fun hf => one_ne_zero <| (Nat.odd_of_mod_four_eq_three hf).symm.trans <| FiniteField.even_card_of_char_two hF
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
⊢ IsSquare (-1) ↔ Fintype.card F % 4 ≠ 3
[PROOFSTEP]
have h₁ := FiniteField.odd_card_of_char_ne_two hF
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h₁ : Fintype.card F % 2 = 1
⊢ IsSquare (-1) ↔ Fintype.card F % 4 ≠ 3
[PROOFSTEP]
rw [← quadraticChar_one_iff_isSquare (neg_ne_zero.mpr (one_ne_zero' F)), quadraticChar_neg_one hF,
  χ₄_nat_eq_if_mod_four, h₁]
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h₁ : Fintype.card F % 2 = 1
⊢ (if 1 = 0 then 0 else if Fintype.card F % 4 = 1 then 1 else -1) = 1 ↔ Fintype.card F % 4 ≠ 3
[PROOFSTEP]
simp only [Nat.one_ne_zero, if_false, ite_eq_left_iff, Ne.def, (by decide : (-1 : ℤ) ≠ 1), imp_false, Classical.not_not]
[GOAL]
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h₁ : Fintype.card F % 2 = 1
⊢ -1 ≠ 1
[PROOFSTEP]
decide
[GOAL]
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h₁ : Fintype.card F % 2 = 1
⊢ Fintype.card F % 4 = 1 ↔ ¬Fintype.card F % 4 = 3
[PROOFSTEP]
exact ⟨fun h => ne_of_eq_of_ne h (by decide : 1 ≠ 3), Or.resolve_right (Nat.odd_mod_four_iff.mp h₁)⟩
[GOAL]
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h₁ : Fintype.card F % 2 = 1
h : Fintype.card F % 4 = 1
⊢ 1 ≠ 3
[PROOFSTEP]
decide
