Module

TeichmullerReduction.lean

Nyll.ValuedFieldTheory.LocalField.Padic.TeichmullerReduction

1 declaration indexed from sourceView source ↗

Module documentation

Teichmüller representatives at finite prime-power levels

A unit modulo a positive power of p whose (p - 1)-st power is one is the reduction of the Teichmüller representative of its residue.

Imports3

Imported by2

theorem

toZModPow_teichmullerUnits_eq

L21 ↗

LocalFieldTheory.DiscreteValuationField.Examples.Qp.toZModPow_teichmullerUnits_eq

Documentation

Prime-to-p roots of order dividing p - 1 are recovered by lifting their residue.

Source context 1 command

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

namespace LocalFieldTheory.DiscreteValuationField.Examples.Qp

Lean source · statement

theorem toZModPow_teichmullerUnits_eq
    (p : ℕ) [Fact p.Prime] (s : ℕ) (u : (ZMod (p ^ (s + 1)))ˣ)
    (hu : u ^ (p - 1) = 1) :
    Units.map (PadicInt.toZModPow (s + 1)).toMonoidHom
      (teichmullerUnits p (ZMod.unitsMap (dvd_pow_self p (Nat.succ_ne_zero s)) u)) = u

Module documentation

Teichmüller representatives at finite prime-power levels

Declarations

toZModPow_teichmullerUnits_eq