Module

PrimePowerExponent.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnitPadicAction.PrimePowerExponent

3 declarations indexed from sourceView source ↗

Module documentation

Prime-power exponents without a finite residue field

Taking a residue-characteristic power moves a positive principal-unit level one step deeper. Iteration kills U^1 / U^(n+1) by p^n, even when the residue field and the level quotients are infinite.

Imports2

Imported by2

theorem

pow_prime_pow_mem

L27 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.pow_prime_pow_mem

Documentation

Iterating the prime-binomial containment moves U^r into U^(r+n).

Source context 5 commands

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

namespace LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
universe u v
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
variable (p : ℕ) [Fact p.Prime] [CharP F.residueField p]

Lean source · statement

theorem pow_prime_pow_mem {r : ℕ} (hr : 1 ≤ r)
    {x : F.valuationSubringˣ} (hx : x ∈ higherPrincipalUnitGroup F r) (n : ℕ) :
    x ^ (p ^ n) ∈ higherPrincipalUnitGroup F (r + n)

theorem

principalUnitQuotientCarrier_pow_prime_pow_eq_one

L39 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitQuotientCarrier_pow_prime_pow_eq_one

Documentation

The n-th principal-unit quotient is killed by p^n.

Source context 5 commands

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

namespace LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
universe u v
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
variable (p : ℕ) [Fact p.Prime] [CharP F.residueField p]

Lean source · statement

theorem Internal.principalUnitQuotientCarrier_pow_prime_pow_eq_one
    (n : ℕ) (x : Internal.principalUnitQuotientCarrier F n) :
    x ^ (p ^ n) = 1

theorem

nsmul_prime_pow_eq_zero

L50 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.DiscretePrincipalUnitQuotient.nsmul_prime_pow_eq_zero

Documentation

The same exponent bound on the canonical discrete additive coordinate.

Source context 5 commands

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

namespace LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
universe u v
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
variable (p : ℕ) [Fact p.Prime] [CharP F.residueField p]

Lean source · statement

theorem DiscretePrincipalUnitQuotient.nsmul_prime_pow_eq_zero
    (n : ℕ) (x : DiscretePrincipalUnitQuotient F n) : (p ^ n) • x = 0

Module documentation

Prime-power exponents without a finite residue field

Declarations

pow_prime_pow_mem

principalUnitQuotientCarrier_pow_prime_pow_eq_one

nsmul_prime_pow_eq_zero