The archimedean Hilbert symbol over ℝ

Over the reals the Hilbert symbol (a,b)_ℝ is -1 exactly when both a and b are negative, and 1 otherwise (for nonzero arguments). Geometrically, the conic z² - a x² - b y² = 0 has a nonzero real point precisely when at least one of a, b is positive: a positive a gives (√a, 1, 0), a positive b gives (√b, 0, 1), while two negative coefficients force z² ≤ 0, hence z = x = y = 0.

theorem HasseMinkowski.hilbertSym_real_eq {a b : ℝ} (ha : a ≠ 0) (hb : b ≠ 0) : hilbertSym a b = if 0 < a ∨ 0 < b then 1 else -1

theorem HasseMinkowski.hilbertSym_real_mul_left (a a' b : ℝ) : hilbertSym (a * a') b = hilbertSym a b * hilbertSym a' b

instance HasseMinkowski.instHasBilinHilbertSymReal : HasBilinHilbertSym ℝ

The real numbers carry a bilinear Hilbert symbol.