NYLL
Module

PrimePowerRoots.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.PrimePowerRoots
2 declarations indexed from sourceView source ↗

Module documentation

Cyclotomic valuation bounds in discrete valuation rings

Evaluating the prime-power cyclotomic polynomial at one gives the valuation formula. In residue characteristic p, a p-power root reduces to one, giving the positive valuation needed to bound the cyclotomic degree.

Imports5
  • Mathlib.Algebra.CharP.Reduced
  • Mathlib.RingTheory.DiscreteValuationRing.Basic
  • Mathlib.RingTheory.LocalRing.ResidueField.Basic
  • Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
  • Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Imported by2

Declarations

theorem

addVal_prime_eq_totient_nsmul

L27 ↗
ValuationTheory.DiscreteValuationField.addVal_prime_eq_totient_nsmul
Documentation

The ramification valuation is the cyclotomic degree times the valuation of the difference between a primitive prime-power root and one.

Source context 2 commands

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

namespace ValuationTheory.DiscreteValuationField
variable {R : Type*} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
Lean source · statement
theorem addVal_prime_eq_totient_nsmul (p n : ℕ) [Fact p.Prime]
    {ζ : R} (hζ : IsPrimitiveRoot ζ (p ^ (n + 1))) :
    IsDiscreteValuationRing.addVal R (p : R) =
      Nat.totient (p ^ (n + 1)) • IsDiscreteValuationRing.addVal R (ζ - 1)
theorem

primePower_totient_le_addVal

L67 ↗
ValuationTheory.DiscreteValuationField.primePower_totient_le_addVal
Documentation

In residue characteristic p, the existence of a primitive p^(n+1)-th root forces its cyclotomic degree to be at most the ramification valuation.

Source context 2 commands

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

namespace ValuationTheory.DiscreteValuationField
variable {R : Type*} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
Lean source · statement
theorem primePower_totient_le_addVal (p n : ℕ) [Fact p.Prime]
    [CharP (IsLocalRing.ResidueField R) p]
    {ζ : R} (hζ : IsPrimitiveRoot ζ (p ^ (n + 1))) :
    (Nat.totient (p ^ (n + 1)) : ℕ∞) ≤ IsDiscreteValuationRing.addVal R (p : R)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.