Module

FinitePrimePowerRoots.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FinitePrimePowerRoots

5 declarations indexed from sourceView source ↗

Module documentation

Finiteness of prime-power roots in mixed-characteristic discrete valuation fields

Roots of unity belong to the valuation ring. The cyclotomic valuation bound gives a single exponent annihilating every root of prime-power order, so they form a finite set.

Imports4

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.Basic
Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.PrimePowerRoots
Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Mathlib.Data.Nat.Totient

Imported by5

theorem

root_mem_valuationSubring

L26 ↗

ValuationTheory.DiscreteValuationField.DVF.root_mem_valuationSubring

Documentation

Every root of unity of positive order lies in the valuation ring.

Source context 3 commands

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

namespace ValuationTheory.DiscreteValuationField
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem DVF.root_mem_valuationSubring (F : DVF.{u, v} K)
    {n : ℕ} (hn : n ≠ 0) {ζ : K} (hζ : ζ ^ n = 1) :
    ζ ∈ F.valuation.valuationSubring

theorem

primePower_exponent_le_totient

L35 ↗

ValuationTheory.DiscreteValuationField.primePower_exponent_le_totient

Documentation

The totient of a positive prime power bounds its exponent.

Source context 3 commands

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

namespace ValuationTheory.DiscreteValuationField
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem primePower_exponent_le_totient {p : ℕ} (hp : p.Prime) (n : ℕ) :
    n + 1 ≤ Nat.totient (p ^ (n + 1))

theorem

primePower_pow_eq_one_of_exists

L47 ↗

ValuationTheory.DiscreteValuationField.primePower_pow_eq_one_of_exists

Documentation

A single exponent, determined by the ramification valuation, annihilates every prime-power root of unity in a mixed-characteristic DVR.

Source context 5 commands

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

namespace ValuationTheory.DiscreteValuationField
universe u v
variable {K : Type u} [Field K]
section ValuationRing
variable {R : Type*} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [CharZero R]

Lean source · statement

theorem primePower_pow_eq_one_of_exists (p : ℕ) [Fact p.Prime]
    [CharP (IsLocalRing.ResidueField R) p]
    {ζ : R} (hζ : ∃ n : ℕ, ζ ^ (p ^ n) = 1) :
    ζ ^ (p ^ (IsDiscreteValuationRing.addVal R (p : R)).toNat) = 1

theorem