The Hilbert symbol

Defines the Hilbert symbol (a,b)_k, valued in {0, ±1}, for a field k, together with its basic vanishing, symmetry and value-set properties, and the class HasBilinHilbertSym recording multiplicativity in the first argument.

noncomputable def HasseMinkowski.hilbertSym {k : Type u_1} [Field k] (a b : k) : ℤ

The Hilbert symbol (a,b)_k, valued in {0, ±1}.

Equations

• HasseMinkowski.hilbertSym a b = if a = 0 ∨ b = 0 then 0 else if ∃ (z : k) (x : k) (y : k), (z, x, y) ≠ (0, 0, 0) ∧ z ^ 2 - a * x ^ 2 - b * y ^ 2 = 0 then 1 else -1

theorem HasseMinkowski.hilbertSym_zero_left {k : Type u_1} [Field k] (a : k) : hilbertSym 0 a = 0

theorem HasseMinkowski.hilbertSym_zero_right {k : Type u_1} [Field k] (a : k) : hilbertSym a 0 = 0

theorem HasseMinkowski.hilbertSym_eq_zero_iff {k : Type u_1} [Field k] (a b : k) : hilbertSym a b = 0 ↔ a = 0 ∨ b = 0

theorem HasseMinkowski.hilbertSym_eq_one_or {k : Type u_1} [Field k] (a b : k) : hilbertSym a b = 1 ∨ hilbertSym a b = 0 ∨ hilbertSym a b = -1

theorem HasseMinkowski.hilbertSym_eq_neg_one_or {k : Type u_1} [Field k] (a b : k) : hilbertSym a b = -1 ∨ hilbertSym a b = 0 ∨ hilbertSym a b = 1

theorem HasseMinkowski.hilbertSym_comm {k : Type u_1} [Field k] (a b : k) : hilbertSym a b = hilbertSym b a

class HasseMinkowski.HasBilinHilbertSym (k : Type u_1) [Field k] : Prop

A field carries a bilinear Hilbert symbol if the symbol is multiplicative in its first argument.

• mul_left_eq {a a' b : k} : hilbertSym (a * a') b = hilbertSym a b * hilbertSym a' b

theorem HasseMinkowski.HasBilinHilbertSym.mul_right_eq {k : Type u_1} [Field k] [HasBilinHilbertSym k] {a b b' : k} : hilbertSym a (b * b') = hilbertSym a b * hilbertSym a b'