K : Type ?u.1283171
R : Type ?u.1283174
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ IsSquare (Units.mk0 a ha) ↔ IsSquare a
K : Type ?u.1283171
R : Type ?u.1283174
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
apply
  (iff_congr _ (by simp [Units.ext_iff])).mp (FiniteField.unit_isSquare_iff hF (Units.mk0 a ha))
K : Type ?u.1283171
R : Type ?u.1283174
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ (∃ r, a = ↑r * ↑r) ↔ ∃ r, a = r * r
K : Type ?u.1283171
R : Type ?u.1283174
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ IsSquare (Units.mk0 a ha) ↔ IsSquare a
simp only [IsSquare, Units.ext_iff, Units.val_mk0, Units.val_mul]
case mp
K : Type ?u.1283171
R : Type ?u.1283174
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ (∃ r, a = ↑r * ↑r) → ∃ r, a = r * r

case mpr
K : Type ?u.1283171
R : Type ?u.1283174
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ (∃ r, a = r * r) → ∃ r, a = ↑r * ↑r
K : Type ?u.1283171
R : Type ?u.1283174
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ (∃ r, a = ↑r * ↑r) ↔ ∃ r, a = r * r
constructor
no goals
K : Type ?u.1283171
R : Type ?u.1283174
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ Units.mk0 a ha ^ (Fintype.card F / 2) = 1 ↔ a ^ (Fintype.card F / 2) = 1
simp [Units.ext_iff]
case mp.intro
K : Type ?u.1283171
R : Type ?u.1283174
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
y : Fˣ
hy : a = ↑y * ↑y
⊢ ∃ r, a = r * r
case mp
K : Type ?u.1283171
R : Type ?u.1283174
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ (∃ r, a = ↑r * ↑r) → ∃ r, a = r * r
rintro ⟨y, hy⟩
no goals
case mp.intro
K : Type ?u.1283171
R : Type ?u.1283174
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
y : Fˣ
hy : a = ↑y * ↑y
⊢ ∃ r, a = r * r
exact ⟨y, hy⟩
case mpr.intro
K : Type ?u.1283171
R : Type ?u.1283174
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
y : F
ha : y * y ≠ 0
⊢ ∃ r, y * y = ↑r * ↑r
case mpr
K : Type ?u.1283171
R : Type ?u.1283174
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ (∃ r, a = r * r) → ∃ r, a = ↑r * ↑r
rintro ⟨y, rfl⟩
case mpr.intro
K : Type ?u.1283171
R : Type ?u.1283174
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
y : F
ha : y * y ≠ 0
hy : y ≠ 0
⊢ ∃ r, y * y = ↑r * ↑r
case mpr.intro
K : Type ?u.1283171
R : Type ?u.1283174
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
y : F
ha : y * y ≠ 0
⊢ ∃ r, y * y = ↑r * ↑r
have hy : y ≠ 0 := by rintro rfl; simp at ha
case mpr.intro
K : Type ?u.1283171
R : Type ?u.1283174
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
y : F
ha : y * y ≠ 0
hy : y ≠ 0
⊢ y * y = ↑(Units.mk0 y hy) * ↑(Units.mk0 y hy)
case mpr.intro
K : Type ?u.1283171
R : Type ?u.1283174
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
y : F
ha : y * y ≠ 0
hy : y ≠ 0
⊢ ∃ r, y * y = ↑r * ↑r
refine' ⟨Units.mk0 y hy, _⟩
no goals
case mpr.intro
K : Type ?u.1283171
R : Type ?u.1283174
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
y : F
ha : y * y ≠ 0
hy : y ≠ 0
⊢ y * y = ↑(Units.mk0 y hy) * ↑(Units.mk0 y hy)
simp
K : Type ?u.1283171
R : Type ?u.1283174
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
ha : 0 * 0 ≠ 0
⊢ False
K : Type ?u.1283171
R : Type ?u.1283174
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
y : F
ha : y * y ≠ 0
⊢ y ≠ 0
rintro rfl
no goals
K : Type ?u.1283171
R : Type ?u.1283174
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
ha : 0 * 0 ≠ 0
⊢ False
simp at ha