Module

LastPrimePowerRoot.lean

Nyll.GaloisCohomology.Kummer.Concrete.LastPrimePowerRoot

2 declarations indexed from sourceView source ↗

Module documentation

The last prime-power root level

Finiteness of the prime-power roots gives a maximal primitive-root exponent. At this exponent a primitive root of prime order has nonidentity power class.

Imports4

Nyll.GaloisCohomology.Kummer.Concrete.PrimePowerRootObstruction
Mathlib.Data.Nat.Basic
Mathlib.Data.Set.Finite.Lemmas
Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Imported by4

theorem

exists_last_primePower_primitiveRoot

L25 ↗

KummerTheory.exists_last_primePower_primitiveRoot

Documentation

A finite set of prime-power roots has a last primitive-root level. The maximality statement also bounds every other available level.

Source context 2 commands

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

namespace KummerTheory
variable {K : Type*} [Field K]

Lean source · statement

theorem exists_last_primePower_primitiveRoot {p : ℕ} (hp : p.Prime)
    (hfinite : Set.Finite {ζ : K | ∃ n : ℕ, ζ ^ (p ^ n) = 1}) :
    ∃ s : ℕ, (primitiveRoots (p ^ s) K).Nonempty ∧
      (∀ m : ℕ, (primitiveRoots (p ^ m) K).Nonempty → m ≤ s) ∧
      ¬ (primitiveRoots (p ^ (s + 1)) K).Nonempty

theorem

exists_last_primePowerRoot_nontrivial_class

L51 ↗

KummerTheory.exists_last_primePowerRoot_nontrivial_class