The Hilbert symbol and norms from k(√b)

For a field k, nonzero a b : k with b not a square, the Hilbert symbol (a,b)_k equals 1 exactly when a is the norm of an element of the quadratic algebra k(√b), realised here as QuadraticAlgebra k b 0 (the algebra with ω² = b). Its norm form is norm ⟨X, Y⟩ = X² - b Y², so this says precisely that the ternary form z² - a x² - b y² has a nontrivial zero.

The key point is the elementary equivalence between a nontrivial zero of z² - a x² - b y² and a being a norm: if x ≠ 0 we divide the equation by x²; if x = 0 then the equation reads z² = b y², which forces b to be a square unless y = z = 0, contradicting nontriviality.

theorem HasseMinkowski.hilbertSym_eq_one_iff_sol {k : Type u_1} [Field k] {a b : k} (ha : a ≠ 0) (hb : b ≠ 0) : hilbertSym a b = 1 ↔ ∃ (z : k) (x : k) (y : k), (z, x, y) ≠ (0, 0, 0) ∧ z ^ 2 - a * x ^ 2 - b * y ^ 2 = 0

theorem HasseMinkowski.hilbertSym_eq_one_iff_isNorm {k : Type u_1} [Field k] {a b : k} (ha : a ≠ 0) (hb : b ≠ 0) (hbsq : ¬IsSquare b) : hilbertSym a b = 1 ↔ ∃ (t : QuadraticAlgebra k b 0), a = QuadraticAlgebra.norm t