Norm valuation at a finite quadratic defect #
An optimal square approximation to a nonsquare a gives a norm from K(√a) whose normalized
valuation is the defect exponent: if a - ξ² = x, then ξ² - a = -x is the norm of ξ + √a.
This supplies a norm witness for any finite quadratic defect exponent.
References #
- O. T. O'Meara, Introduction to Quadratic Forms, §63A.
theorem
TauCeti.exists_mem_quadraticNormSubgroup_toAdd_normalizedValuation_eq_defectExponent
{K : Type u_1}
[Field K]
[ValuativeRel K]
[TopologicalSpace K]
[IsNonarchimedeanLocalField K]
{a : Kˣ}
{d : ℤ}
(hd : defectExponent a = ↑d)
:
∃ b ∈ quadraticNormSubgroup ↑a, Multiplicative.toAdd ((normalizedValuation K) b) = d
If the quadratic defect of a has finite exponent d, then some norm from K(√a) has
normalized valuation exactly d.