Module

NonmonicSimpleRoot.lean

Nyll.ValuedFieldTheory.Valuation.Henselian.NonmonicSimpleRoot

1 declaration indexed from sourceView source ↗

Module documentation

Simple roots of nonmonic polynomials over Henselian valuation rings

A simple residual root gives a coprime linear factor. Primitive factor lifting produces an actual factor of degree one. Its leading coefficient reduces to one, so it is a unit and its linear root belongs to the valuation ring.

Imports4

Nyll.ValuedFieldTheory.Valuation.Henselian.SimpleRootFactorization
Nyll.ValuedFieldTheory.Valuation.Henselian.Core
Mathlib.Algebra.Polynomial.Degree.SmallDegree
Mathlib.RingTheory.LocalRing.RingHom.Basic

Imported by3

theorem

exists_root_of_henselianRing_of_simpleRoot_mod

L29 ↗

DiscreteValuationField.exists_root_of_henselianRing_of_simpleRoot_mod

Documentation

A simple residual root lifts for an arbitrary polynomial over a Henselian valuation ring. No monicity or completeness assumption is needed.

Source context 3 commands

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

namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
variable {K : Type*} [Field K] (V : ValuationSubring K)
  [HenselianRing V (IsLocalRing.maximalIdeal V)]

Lean source · statement

theorem exists_root_of_henselianRing_of_simpleRoot_mod
    (f : Polynomial V) (a₀ : V)
    (hroot : f.eval a₀ ∈ IsLocalRing.maximalIdeal V)
    (hsimple : IsUnit
      (Ideal.Quotient.mk (IsLocalRing.maximalIdeal V) (f.derivative.eval a₀))) :
    ∃ a : V, f.IsRoot a ∧ a - a₀ ∈ IsLocalRing.maximalIdeal V

Module documentation

Simple roots of nonmonic polynomials over Henselian valuation rings

Declarations

exists_root_of_henselianRing_of_simpleRoot_mod