Module

Gather.lean

Nyll.GaloisCohomology.Kummer.Concrete.Cyclotomic.ProfiniteUnitDecomposition.Gather

1 declaration indexed from sourceView source ↗

Module documentation

Imports1

Imported by4

def

KummerTheory.ProfiniteUnitDecomposition.Internal.gatherFree

Documentation

Reassemble the family of local additive coordinates into ℤ̂.

Source context 5 commands

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

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

Lean source · statement

def gatherFree :
    ((p : Nat.Primes) → Multiplicative ℤ_[p.1]) ≃ₜ*
      Multiplicative ZHat