GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldGaloisContinuousEquivNormQuotient_apply
Evaluation of the selected class-field equivalence is the named inverse global norm-residue value in the quotient by the defining subgroup.
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
closedFiniteIndexClassFieldGaloisContinuousEquivNormQuotient_apply
(H : Subgroup (IdeleClassGroup K))
(hclosed : IsClosed (H : Set (IdeleClassGroup K)))
[H.FiniteIndex]
(σ : Gal((closedFiniteIndexClassField
(K := K) H hclosed)/K)) :
closedFiniteIndexClassFieldGaloisContinuousEquivNormQuotient
(K := K) H hclosed σ =
closedFiniteIndexClassFieldReciprocityValue
(K := K) H hclosed σ