theorem legendreSym_val {p : ℕ} [hp : Fact (Nat.Prime p)] (a : ZMod p) : legendreSym p ↑a.val = (quadraticChar (ZMod p)) a

The Legendre symbol on the natural-number value of a : ZMod p agrees with the quadratic character of ZMod p.

theorem padic_hilbert_mul_left (p : ℕ) [Fact (Nat.Prime p)] (a b c : ℚ_[p]ˣ) : padicHilbertSymbol p (a * b) c = padicHilbertSymbol p a c * padicHilbertSymbol p b c

Bilinearity of the $p$-adic Hilbert symbol in the left argument: $(ab, c)_p = (a, c)_p \cdot (b, c)_p$ (part of Corollary 10.10).