Module

PadicReductionContinuous.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnitPadicAction.PadicReductionContinuous

2 declarations indexed from sourceView source ↗

Module documentation

Continuity of reduction of p-adic integers

Reduction modulo p^n has open kernel and is continuous for the discrete topology on the quotient. This source has no local-field dependencies.

Imports3

Mathlib.NumberTheory.Padics.RingHoms
Mathlib.Topology.Algebra.Group.Basic
Mathlib.Topology.MetricSpace.Ultra.Basic

Imported by5

theorem

isOpen_ker_padicIntToZModPow

L23 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.isOpen_ker_padicIntToZModPow

Documentation

The kernel of reduction Z_p -> ZMod (p^n) is open.

Source context 1 command

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

namespace LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup

Lean source · statement

theorem isOpen_ker_padicIntToZModPow
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    IsOpen
      ((RingHom.ker (PadicInt.toZModPow n : ℤ_[p] →+* ZMod (p ^ n)) :
        Ideal ℤ_[p]) : Set ℤ_[p])

theorem

continuous_padicIntToZModPow

L46 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.continuous_padicIntToZModPow