WIP: Import Local and global class field theory

LeanPool/ClassFieldTheory/ClassFieldTheory.lean

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2026 n-yamaguchi-0729. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: n-yamaguchi-0729
+-/
+module
+
+
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.Algebra
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AlgebraicNumberTheory
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.All
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.Definitions
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.GlobalClassFieldTheory
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.HasseArf
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.KroneckerWeber
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.KummerTheory
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.LocalClassFieldTheory
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.LocalFieldTheory
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.LubinTate
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.RamificationTheory
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.Theorems
+
+/-! Supporting modules for Local and global class field theory. -/
+

LeanPool/ClassFieldTheory/ClassFieldTheory/AbstractClassFieldTheory.lean

@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2026 n-yamaguchi-0729. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: n-yamaguchi-0729
+-/
+module
+
+
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.All
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity
+
+/-! Supporting modules for Local and global class field theory. -/
+

LeanPool/ClassFieldTheory/ClassFieldTheory/AbstractClassFieldTheory/All.lean

@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2026 n-yamaguchi-0729. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: n-yamaguchi-0729
+-/
+module
+
+
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.All
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.All
+/-!
+# Abstract class field theory
+
+Public root for abstract degree data, class formations, reciprocity, and the construction and
+naturality of Artin maps. The public declarations live in the `ClassFormation` namespace. This
+library is independent of local class field theory.
+
+The representation-free degree, field, extension, and topological-generation
+APIs are universe-polymorphic.  The boundary that uses Mathlib's `Rep ℤ G` is
+necessarily universe zero because `Rep` currently places its coefficient ring
+and acting group in the same universe; the affected source sections state that
+constraint explicitly.
+-/
+

LeanPool/ClassFieldTheory/ClassFieldTheory/AbstractClassFieldTheory/Degree.lean

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2026 n-yamaguchi-0729. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: n-yamaguchi-0729
+-/
+module
+
+
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.All
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.Fields
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.Frobenius
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.FrobeniusFixedField
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.FrobeniusLift
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.Indices
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.Norm
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.NormConjugation
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.NormLaws
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.PadicCyclicClosure
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.PrimeElements
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.ProfiniteIntegerFiniteQuotient
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.Valuation
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.ValuationLaws
+
+/-! Supporting modules for Local and global class field theory. -/
+

LeanPool/ClassFieldTheory/ClassFieldTheory/AbstractClassFieldTheory/Degree/All.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2026 n-yamaguchi-0729. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: n-yamaguchi-0729
+-/
+module
+
+
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.Fields
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.Frobenius
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.FrobeniusFixedField
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.FrobeniusLift
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.Indices
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.Norm
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.NormConjugation
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.NormLaws
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.PadicCyclicClosure
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.PrimeElements
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.ProfiniteIntegerFiniteQuotient
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.Valuation
+public import LeanPool.ClassFieldTheory.ClassFieldTheory.AbstractClassFieldTheory.Degree.ValuationLaws
+/-!
+# Degree and valuation data
+
+Focused aggregate for abstract fields, normalized degrees, Frobenius, norms, prime elements, and
+valuation laws used by class formations.
+-/
+