ClassFieldTheory.GlobalHilbertPairingFamily.finiteFactor
Evaluate a local pairing on two nonzero elements of the number field and transport the resulting root of unity back to the number field.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalHilbertPairingFamily
universe uLean source · statement
def finiteFactor
(F : Type u) [Field F] [NumberField F]
{n : ℕ+} (B : GlobalHilbertPairingFamily F n)
(hmu : (primitiveRoots (n : ℕ) F).Nonempty)
(v : HeightOneSpectrum (𝓞 F)) (a b : Fˣ) :
rootsOfUnity (n : ℕ) F