NYLL
Module

DivisionBounds.lean

Nyll.ValuedFieldTheory.Valuation.Henselian.Factorization.DivisionBounds
2 declarations indexed from sourceView source ↗

Module documentation

degree bounds for the division remainder

This file supplies the degree estimate for the remainder in the coefficientwise Hensel correction step. It removes the later need to assume separately that the residue of the remainder has small degree.

Imports1
Imported by10

Declarations

theorem

henselFactorization_remainder_natDegree_le_of_degree_lt

L26 ↗
AlgebraicNumberTheory.Valuations.henselFactorization_remainder_natDegree_le_of_degree_lt
Documentation

the remainder estimate before reducing coefficients.

Source context 4 commands

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

noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace Valuations
Lean source · statement
theorem henselFactorization_remainder_natDegree_le_of_degree_lt
    {R : Type*} [CommRing R] {g0 p : R[X]} {m : ℕ}
    (hg0nat : g0.natDegree = m) (hpdeg : p.degree < g0.degree) :
    p.natDegree ≤ m
theorem

henselFactorization_residue_remainder_natDegree_le_of_degree_lt

L42 ↗
AlgebraicNumberTheory.Valuations.henselFactorization_residue_remainder_natDegree_le_of_degree_lt
Documentation

the remainder estimate in residue-degree form: if the division remainder has degree strictly smaller than g0, and g0 has natural degree m, then the residue of the remainder has natural degree at most m.

Source context 4 commands

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

noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace Valuations
Lean source · statement
theorem henselFactorization_residue_remainder_natDegree_le_of_degree_lt
    {R : Type*} [CommRing R] [IsLocalRing R]
    {g0 p : R[X]} {m : ℕ}
    (hg0nat : g0.natDegree = m) (hpdeg : p.degree < g0.degree) :
    (p.map (IsLocalRing.residue R)).natDegree ≤ m

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.