KummerTheory.ProfiniteUnitDecomposition.Internal.freeFiniteSwap
Swap the collected free and finite coordinates.
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 _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup (
continuousMulEquivProdComm
) inLean source · statement
def freeFiniteSwap :
CyclotomicFinitePart × Multiplicative ZHat ≃ₜ*
Multiplicative ZHat × CyclotomicFinitePart