NYLL
Module

ReductionCompatibility.lean

Nyll.ValuedFieldTheory.LocalField.Padic.ReductionCompatibility
2 declarations indexed from sourceView source ↗

Module documentation

Compatibility of reduction modulo prime powers and modulo the prime

Reduction from the p-adic integers through a positive prime-power quotient agrees with their residue map to ZMod p.

Imports3
  • Mathlib.NumberTheory.Padics.RingHoms
  • Mathlib.Data.ZMod.Units
  • Mathlib.RingTheory.LocalRing.RingHom.Basic
Imported by2

Declarations

theorem

toZMod_comp_toZModPow

L22 ↗
LocalFieldTheory.DiscreteValuationField.toZMod_comp_toZModPow
Documentation

Reducing modulo a positive prime power and then modulo the prime is the usual p-adic residue map.

Source context 1 command

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

namespace LocalFieldTheory.DiscreteValuationField
Lean source · statement
theorem toZMod_comp_toZModPow (p : ℕ) [Fact p.Prime] (s : ℕ) :
    (ZMod.castHom (dvd_pow_self p (Nat.succ_ne_zero s)) (ZMod p)).comp
      (PadicInt.toZModPow (s + 1)) = PadicInt.toZMod
theorem

unitsMap_toZModPow

L30 ↗
LocalFieldTheory.DiscreteValuationField.unitsMap_toZModPow
Documentation

The same compatibility on the actual unit groups.

Source context 1 command

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

namespace LocalFieldTheory.DiscreteValuationField
Lean source · statement
theorem unitsMap_toZModPow (p : ℕ) [Fact p.Prime] (s : ℕ) (u : ℤ_[p]ˣ) :
    ZMod.unitsMap (dvd_pow_self p (Nat.succ_ne_zero s))
      (Units.map (PadicInt.toZModPow (s + 1)).toMonoidHom u) =
        Units.map PadicInt.toZMod.toMonoidHom u

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