GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldGaloisEquivNormQuotient_apply
Evaluation of the direct non-topological reciprocity equivalence.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
variable {K : Type} [Field K] [NumberField K]Lean source · statement
theorem closedFiniteIndexClassFieldGaloisEquivNormQuotient_apply
(H : Subgroup (IdeleClassGroup K))
(hclosed : IsClosed (H : Set (IdeleClassGroup K)))
[H.FiniteIndex]
(σ : Gal((closedFiniteIndexClassField
(K := K) H hclosed)/K)) :
closedFiniteIndexClassFieldGaloisEquivNormQuotient
(K := K) H hclosed σ =
closedFiniteIndexClassFieldReciprocityValue
(K := K) H hclosed σ