Module

DyadicNorm.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.DyadicNorm

1 declaration indexed from sourceView source ↗

Module documentation

Dyadic quadratic norm forms

The normalized valuation and its uniformizer are constructed from the original valuation ring. Thus the norm obstruction needs only the Henselian discrete valuation and residue characteristic two.

Imports4

Imported by2

theorem

exists_quadraticForm_outside_squareClasses

L26 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.exists_quadraticForm_outside_squareClasses

Documentation

Every nontrivial quadratic square class over a Henselian dyadic DVF has a norm outside the two square classes that become squares in the quadratic extension.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ValuationTheory.DiscreteValuationField.HenselianDVF
universe u v

Lean source · statement

theorem exists_quadraticForm_outside_squareClasses
    {K : Type u} [Field K] [CharZero K]
    (base : HenselianDVF.{u, v} K) [CharP base.residueField 2]
    (a : K) (ha : ¬ IsSquare a) :
    ∃ x y : K, ¬ IsSquare (x ^ 2 - a * y ^ 2) ∧
      ¬ IsSquare ((x ^ 2 - a * y ^ 2) / a)

Module documentation

Dyadic quadratic norm forms

Declarations

exists_quadraticForm_outside_squareClasses