Module

LocalHilbertPairingInverse.lean

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.LocalHilbertPairingInverse

1 declaration indexed from sourceView source ↗

Module documentation

Inverting the values of a local Hilbert pairing

The algebraic laws and norm-vanishing criterion are invariant under inversion of every value. Thus these conditions alone do not distinguish the value convention used by a normalized local Artin map. This theorem does not assert that a pairing and its inverse are distinct.

Imports2

Nyll.ClassFieldTheory.Definitions.HilbertSymbols.IsLocalHilbertPairing
Mathlib.Algebra.Group.Hom.Basic

Imported by1

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.All

theorem

inv

L24 ↗

ClassFieldTheory.HilbertPairing.IsLocalHilbertPairing.inv

Documentation

Inverting every value preserves the local Hilbert-pairing axioms.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ClassFieldTheory.HilbertPairing
universe u

Lean source · statement

theorem IsLocalHilbertPairing.inv
    {K : Type u} [Field K] {n : ℕ+}
    {B : HilbertPairing K n}
    (hB : B.IsLocalHilbertPairing) :
    (B⁻¹).IsLocalHilbertPairing

Module documentation

Inverting the values of a local Hilbert pairing

Declarations

inv