The Hilbert symbol over algebraically closed fields

This file computes the norm-equation Hilbert symbol TauCeti.hilbertSymbol over algebraically closed fields. Every element is a square, so the symbol is always 1.

Main results

• TauCeti.hilbertSymbol_eq_one_of_isAlgClosed: the symbol is trivial over an algebraically closed field.

References

• J.-P. Serre, A Course in Arithmetic, Chapter III, §1.1.
• O. T. O'Meara, Introduction to Quadratic Forms, 71:18.

@[simp]

theorem TauCeti.hilbertSymbol_eq_one_of_isAlgClosed {K : Type u_1} [Field K] [IsAlgClosed K] (a b : Kˣ) : hilbertSymbol a b = 1

Over an algebraically closed field, such as ℂ, the Hilbert symbol is always 1.