Module

ClosedAddSubgroup.lean

Nyll.ValuedFieldTheory.LocalField.Padic.ClosedAddSubgroup

3 declarations indexed from sourceView source ↗

Module documentation

Closed additive subgroups of the p-adic integers

A nonzero closed additive subgroup of ℤ_[p] contains a nonzero principal ideal. Since every nonzero ideal of ℤ_[p] is generated by a power of p, such a subgroup is open.

Imports2

Mathlib.NumberTheory.Padics.RingHoms
Mathlib.Topology.Algebra.OpenSubgroup

Imported by3

theorem

addSubgroup_isOpen_of_isClosed_of_ne_bot

L25 ↗

PadicInt.addSubgroup_isOpen_of_isClosed_of_ne_bot

Documentation

A nonzero closed additive subgroup of the p-adic integers is open.

Source context 2 commands

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

open scoped Topology
namespace PadicInt

Lean source · statement

theorem addSubgroup_isOpen_of_isClosed_of_ne_bot
    (p : ℕ) [hp : Fact p.Prime]
    (H : AddSubgroup ℤ_[p])
    (hclosed : IsClosed (H : Set ℤ_[p]))
    (hne : H ≠ ⊥) :
    IsOpen (H : Set ℤ_[p])

theorem

exists_positive_natCast_sub_mem_of_isOpen_addSubgroup

L91 ↗

PadicInt.exists_positive_natCast_sub_mem_of_isOpen_addSubgroup

Documentation

Every additive coset of an open subgroup of the p-adic integers contains the cast of a positive natural number.

The positive natural numbers are dense because they are the translate by one of the dense image of ℕ in ℤ_[p].

Source context 2 commands

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

open scoped Topology
namespace PadicInt

Lean source · statement

theorem exists_positive_natCast_sub_mem_of_isOpen_addSubgroup
    (p : ℕ) [Fact p.Prime]
    (H : AddSubgroup ℤ_[p])
    (hopen : IsOpen (H : Set ℤ_[p]))
    (z : ℤ_[p]) :
    ∃ n : ℕ, 0 < n ∧ z - (n : ℤ_[p]) ∈ H

theorem

multiplicative_positiveNatDegree_ne_one

L120 ↗

PadicInt.multiplicative_positiveNatDegree_ne_one

Documentation

A positive integral degree is nontrivial in the multiplicative copy of the additive group of ℤ_p.

Source context 2 commands

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

open scoped Topology
namespace PadicInt

Lean source · statement

theorem multiplicative_positiveNatDegree_ne_one
    (p : ℕ) [Fact p.Prime]
    (n : ℕ) (hn : 0 < n) :
    (Multiplicative.ofAdd (1 : ℤ_[p])) ^ n ≠ 1

Module documentation

Closed additive subgroups of the p-adic integers

Declarations

addSubgroup_isOpen_of_isClosed_of_ne_bot

exists_positive_natCast_sub_mem_of_isOpen_addSubgroup

multiplicative_positiveNatDegree_ne_one