ClassFieldTheory.HilbertPairing.IsLocalHilbertPairing
The algebraic laws and Kummer norm-residue criterion required of a local Hilbert pairing. These properties do not fix the value normalization of the symbol; that requires a comparison with a normalized Artin map.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTheory.HilbertPairing
universe uLean source · statement
def IsLocalHilbertPairing
{K : Type u} [Field K] {n : ℕ+}
(B : HilbertPairing K n) : Prop