Module

PrimePowerTorsionReduction.lean

Nyll.ValuedFieldTheory.LocalField.Padic.PrimePowerTorsionReduction

1 declaration indexed from sourceView source ↗

Module documentation

Prime-to-p torsion is determined by reduction modulo p

Two units modulo a positive power of p annihilated by the same exponent coprime to p are equal if their reductions modulo p agree. The proof uses uniqueness of a simple polynomial root in a local ring.

Imports3

Mathlib.Data.ZMod.Units
Mathlib.NumberTheory.Padics.RingHoms
Mathlib.RingTheory.Henselian

Imported by2

theorem

primePower_units_eq_of_pow_eq_one_of_reduction_eq

L23 ↗

LocalFieldTheory.DiscreteValuationField.primePower_units_eq_of_pow_eq_one_of_reduction_eq

Documentation

Reduction modulo p distinguishes the prime-to-p roots of unity modulo any positive power of p.

Source context 1 command

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

namespace LocalFieldTheory.DiscreteValuationField

Lean source · statement

theorem primePower_units_eq_of_pow_eq_one_of_reduction_eq
    (p : ℕ) [Fact p.Prime] (s n : ℕ) (hn : n.Coprime p)
    (u v : (ZMod (p ^ (s + 1)))ˣ) (hu : u ^ n = 1) (hv : v ^ n = 1)
    (hred : ZMod.unitsMap (dvd_pow_self p (Nat.succ_ne_zero s)) u =
      ZMod.unitsMap (dvd_pow_self p (Nat.succ_ne_zero s)) v) : u = v

Module documentation

Prime-to-p torsion is determined by reduction modulo p

Declarations

primePower_units_eq_of_pow_eq_one_of_reduction_eq