Module

Decomposition.lean

Nyll.GaloisCohomology.Kummer.Concrete.Cyclotomic.ProfiniteUnitDecomposition.Decomposition

1 declaration indexed from sourceView source ↗

Module documentation

Imports1

Imported by3

def

KummerTheory.zHatUnitsDecomposition

Documentation

Topological decomposition ℤ̂ˣ ≃ Multiplicative ℤ̂ × finite-product used in the rational cyclotomic calculation.

Source context 5 commands

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

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

Lean source · statement

def zHatUnitsDecomposition :
    ZHatˣ ≃ₜ* Multiplicative ZHat × CyclotomicFinitePart