English
If χ is nontrivial quadratic and there is a primitive ψ, then (χ(-1) · |R|)^{(p^n)/2} = χ(p^n).
Русский
Если χ не тривиален квадратичен и есть примитивный ψ, то (χ(-1) · |R|)^{(p^n)/2} = χ(p^n).
LaTeX
$$$\big( χ(-1) \cdot |R| \big)^{\frac{p^n}{2}} = χ(p^n)$$$
Lean4
/-- When `F` and `F'` are finite fields and `χ : F → F'` is a nontrivial quadratic character,
then `(χ(-1) * #F)^(#F'/2) = χ #F'`. -/
theorem card_pow_card {F : Type*} [Field F] [Fintype F] {F' : Type*} [Field F'] [Fintype F'] {χ : MulChar F F'}
(hχ₁ : χ ≠ 1) (hχ₂ : IsQuadratic χ) (hch₁ : ringChar F' ≠ ringChar F) (hch₂ : ringChar F' ≠ 2) :
(χ (-1) * Fintype.card F) ^ (Fintype.card F' / 2) = χ (Fintype.card F') :=
by
obtain ⟨n, hp, hc⟩ := FiniteField.card F (ringChar F)
obtain ⟨n', hp', hc'⟩ := FiniteField.card F' (ringChar F')
let ψ := FiniteField.primitiveChar F F' hch₁
let FF' := CyclotomicField ψ.n F'
have hchar := Algebra.ringChar_eq F' FF'
apply (algebraMap F' FF').injective
rw [map_pow, map_mul, map_natCast, hc', hchar, Nat.cast_pow]
simp only [← MulChar.ringHomComp_apply]
have := Fact.mk hp'
have := Fact.mk (hchar.subst hp')
rw [Ne, ← Nat.prime_dvd_prime_iff_eq hp' hp, ← isUnit_iff_not_dvd_char, hchar] at hch₁
exact
Char.card_pow_char_pow (hχ₂.comp _) ψ.char (ringChar FF') n' hch₁ (hchar ▸ hch₂)
(gaussSum_sq ((ringHomComp_ne_one_iff (RingHom.injective _)).mpr hχ₁) (hχ₂.comp _) ψ.prim)
