Module

Local.lean

Nyll.GaloisCohomology.Kummer.Concrete.Cyclotomic.ProfiniteUnitDecomposition.Local

1 declaration indexed from sourceView source ↗

Module documentation

Imports1

Imported by3

def

KummerTheory.ProfiniteUnitDecomposition.Internal.localDecomposition

Documentation

The product of the local finite/free decompositions, compiled separately from the global coordinate-reassembly stages.

Source context 4 commands

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

open scoped Topology
noncomputable section
namespace KummerTheory.ProfiniteUnitDecomposition.Internal
open LocalFieldTheory.Padic

Lean source · statement

def localDecomposition :
    ((p : Nat.Primes) →
      padicUnitFiniteFactor p.1 × Multiplicative ℤ_[p.1]) ≃ₜ*
    ((p : Nat.Primes) → ℤ_[p.1]ˣ)