ClassFieldTheory.globalInfinitePlaceHilbertSymbol
The Hilbert factor at an infinite place. It is nontrivial only at a real place for the quadratic exponent, when both arguments are negative.
In the product-formula theorem the field contains a primitive n-th root of unity; under that hypothesis real places occur only in the cases covered by this formula.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField
noncomputable section
namespace ClassFieldTheory
universe uLean source · statement
def globalInfinitePlaceHilbertSymbol
(F : Type u) [Field F] [NumberField F]
(n : ℕ+) (v : InfinitePlace F) (a b : Fˣ) :
rootsOfUnity (n : ℕ) F