no goals
K : Type u_1
R : Type ?u.113435
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
ha : a ≠ 0
⊢ a ^ (q - 1) = 1
calc
  a ^ (Fintype.card K - 1) = (Units.mk0 a ha ^ (Fintype.card K - 1) : Kˣ).1 := by
    rw [Units.val_pow_eq_pow_val, Units.val_mk0]
  _ = 1 := by
    classical
      rw [← Fintype.card_units, pow_card_eq_one]
      rfl
no goals
K : Type u_1
R : Type ?u.113435
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
ha : a ≠ 0
⊢ a ^ (q - 1) = ↑(Units.mk0 a ha ^ (q - 1))
rw [Units.val_pow_eq_pow_val, Units.val_mk0]
no goals
K : Type u_1
R : Type ?u.113435
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
ha : a ≠ 0
⊢ ↑(Units.mk0 a ha ^ (q - 1)) = 1
classical
  rw [← Fintype.card_units, pow_card_eq_one]
  rfl
K : Type u_1
R : Type ?u.113435
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
ha : a ≠ 0
⊢ ↑1 = 1
K : Type u_1
R : Type ?u.113435
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
ha : a ≠ 0
⊢ ↑(Units.mk0 a ha ^ (q - 1)) = 1
rw [← Fintype.card_units, pow_card_eq_one]
no goals
K : Type u_1
R : Type ?u.113435
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
ha : a ≠ 0
⊢ ↑1 = 1
rfl