Module

DyadicSquareRoots.lean

Nyll.ValuedFieldTheory.Valuation.DyadicSquareRoots

4 declarations indexed from sourceView source ↗

Module documentation

Square roots and first-order principal units in dyadic valued fields

Hensel's simple-root theorem bounds the precision of a nonsquare near one. For integer-valued valuations, a principal unit of valuation-one difference from one cannot be a square when the value of two is less than one.

Imports7

Mathlib.RingTheory.Henselian
Mathlib.RingTheory.Valuation.ValuationSubring
Mathlib.Algebra.Polynomial.Monic
Mathlib.Tactic.LinearCombination
Mathlib.Tactic.FieldSimp
Mathlib.Data.Int.WithZero
Mathlib.Data.Int.LeastGreatest

Imported by2

theorem

exists_sq_eq_of_valuation_sub_one_lt_two_sq

L27 ↗

ValuationTheory.exists_sq_eq_of_valuation_sub_one_lt_two_sq

Documentation

The substitution b = 1 + 2z reduces the square-root problem to a monic polynomial with derivative one at its residual root.

Source context 1 command

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

namespace ValuationTheory

Lean source · statement

theorem exists_sq_eq_of_valuation_sub_one_lt_two_sq
    {K Γ : Type*} [Field K] [CharZero K] [LinearOrderedCommGroupWithZero Γ]
    (v : Valuation K Γ)
    [HenselianRing v.valuationSubring (IsLocalRing.maximalIdeal v.valuationSubring)]
    (a : K) (ha : v (a - 1) < v (2 : K) ^ 2) :
    ∃ b : K, b ^ 2 = a

theorem

le_exp_neg_one_of_lt_one

L63 ↗

ValuationTheory.le_exp_neg_one_of_lt_one

Source context 1 command

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

namespace ValuationTheory

Lean source · statement

theorem le_exp_neg_one_of_lt_one
    {x : WithZero (Multiplicative ℤ)} (hx : x < 1) :
    x ≤ WithZero.exp (-1 : ℤ)

theorem

not_isSquare_of_valuation_sub_one_eq_exp_neg_one

L78 ↗

ValuationTheory.not_isSquare_of_valuation_sub_one_eq_exp_neg_one

Documentation

A first-order principal unit is not a square in residue characteristic two. Only the inequality for the value of two is needed.

Source context 1 command

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

namespace ValuationTheory

Lean source · statement

theorem not_isSquare_of_valuation_sub_one_eq_exp_neg_one
    {K : Type*} [Field K]
    (v : Valuation K (WithZero (Multiplicative ℤ))) (h2 : v (2 : K) < 1)
    {a : K} (ha : v (a - 1) = WithZero.exp (-1 : ℤ)) :
    ¬ IsSquare a

theorem

exists_minimal_valuation_squareClass_difference

L118 ↗

ValuationTheory.exists_minimal_valuation_squareClass_difference

Documentation

A nonsquare has a square multiple closest to one among multipliers of value one.

Source context 1 command

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

namespace ValuationTheory

Lean source · statement

theorem exists_minimal_valuation_squareClass_difference
    {K : Type*} [Field K] [CharZero K]
    (v : Valuation K (WithZero (Multiplicative ℤ)))
    [HenselianRing v.valuationSubring (IsLocalRing.maximalIdeal v.valuationSubring)]
    (a : Kˣ) (hns : ¬ IsSquare (a : K)) :
    ∃ c : Kˣ, v (c : K) = 1 ∧
      ∀ d : Kˣ, v (d : K) = 1 →
        v ((a : K) * (c : K) ^ 2 - 1) ≤ v ((a : K) * (d : K) ^ 2 - 1)

Module documentation

Square roots and first-order principal units in dyadic valued fields

Declarations

exists_sq_eq_of_valuation_sub_one_lt_two_sq

le_exp_neg_one_of_lt_one

not_isSquare_of_valuation_sub_one_eq_exp_neg_one

exists_minimal_valuation_squareClass_difference