Module

FiniteField.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.PowerResidueSymbols.FiniteField

3 declarations indexed from sourceView source ↗

Module documentation

Power-residue symbols over finite fields

For a finite field k of cardinality q and n ∣ q - 1, the tame power-residue symbol is

u ↦ u ^ ((q - 1) / n).

Its kernel is exactly the subgroup of n-th powers.

Imports2

Mathlib.Algebra.Group.Subgroup.Finite
Mathlib.FieldTheory.Finite.Basic

Imported by3

def

finiteFieldPowerResidueSymbol

L27 ↗

AlgebraicNumberTheory.PowerResidueSymbols.finiteFieldPowerResidueSymbol

Documentation

The finite-field n-th power-residue symbol.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
variable (k : Type*) [Field k] [Fintype k]

Lean source · full declaration

def finiteFieldPowerResidueSymbol
    (n : ℕ+) (hn : (n : ℕ) ∣ Fintype.card k - 1) :
    kˣ →* rootsOfUnity (n : ℕ) k where
  toFun u :=
    ⟨u ^ ((Fintype.card k - 1) / (n : ℕ)), by
      change (u ^ ((Fintype.card k - 1) / (n : ℕ))) ^ (n : ℕ) = 1
      rw [← pow_mul, Nat.div_mul_cancel hn]
      apply Units.ext
      exact FiniteField.pow_card_sub_one_eq_one
        (u : k) (Units.ne_zero u)⟩
  map_one' := by
    apply Subtype.ext
    simp
  map_mul' u v := by
    apply Subtype.ext
    simp [mul_pow]

theorem

finiteFieldPowerResidueSymbol_apply

L45 ↗

AlgebraicNumberTheory.PowerResidueSymbols.finiteFieldPowerResidueSymbol_apply

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
variable (k : Type*) [Field k] [Fintype k]

Lean source · statement

theorem finiteFieldPowerResidueSymbol_apply
    (n : ℕ+) (hn : (n : ℕ) ∣ Fintype.card k - 1) (u : kˣ) :
    ((finiteFieldPowerResidueSymbol k n hn u :
        rootsOfUnity (n : ℕ) k) : kˣ) =
      u ^ ((Fintype.card k - 1) / (n : ℕ))

theorem

finiteFieldPowerResidueSymbol_eq_one_iff

L53 ↗

AlgebraicNumberTheory.PowerResidueSymbols.finiteFieldPowerResidueSymbol_eq_one_iff

Documentation

The finite-field symbol is trivial exactly on n-th powers.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace AlgebraicNumberTheory
namespace PowerResidueSymbols
variable (k : Type*) [Field k] [Fintype k]

Lean source · statement

theorem finiteFieldPowerResidueSymbol_eq_one_iff
    (n : ℕ+) (hn : (n : ℕ) ∣ Fintype.card k - 1) (u : kˣ) :
    finiteFieldPowerResidueSymbol k n hn u = 1 ↔
      ∃ v : kˣ, v ^ (n : ℕ) = u

Module documentation

Power-residue symbols over finite fields

Declarations

finiteFieldPowerResidueSymbol

finiteFieldPowerResidueSymbol_apply

finiteFieldPowerResidueSymbol_eq_one_iff