Distinguished polynomial #
In this file we define the predicate Polynomial.IsDistinguishedAt
and develop the most basic lemmas about it.
structure
Polynomial.IsDistinguishedAt
{R : Type u_1}
[CommRing R]
(f : Polynomial R)
(I : Ideal R)
extends f.IsWeaklyEisensteinAt I :
Given an ideal I
of a commutative ring R
, we say that a polynomial f : R[X]
is Distinguished at I
if f
is monic and IsWeaklyEisensteinAt I
.
i.e. f
is of the form xⁿ + a₁xⁿ⁻¹ + ⋯ + aₙ
with aᵢ ∈ I
for all i
.
- monic : f.Monic
Instances For
theorem
Polynomial.IsDistinguishedAt.map_eq_X_pow
{R : Type u_1}
[CommRing R]
{f : Polynomial R}
{I : Ideal R}
(distinguish : f.IsDistinguishedAt I)
:
@[deprecated Polynomial.IsDistinguishedAt.map_eq_X_pow (since := "2025-04-27")]
theorem
IsDistinguishedAt.map_eq_X_pow
{R : Type u_1}
[CommRing R]
{f : Polynomial R}
{I : Ideal R}
(distinguish : f.IsDistinguishedAt I)
:
theorem
Polynomial.IsDistinguishedAt.degree_eq_order_map
{R : Type u_1}
[CommRing R]
{I : Ideal R}
(f h : PowerSeries R)
{g : Polynomial R}
(distinguish : g.IsDistinguishedAt I)
(nmem : (PowerSeries.constantCoeff R) h ∉ I)
(eq : f = ↑g * h)
:
@[deprecated Polynomial.IsDistinguishedAt.degree_eq_order_map (since := "2025-04-27")]
theorem
IsDistinguishedAt.degree_eq_order_map
{R : Type u_1}
[CommRing R]
{I : Ideal R}
(f h : PowerSeries R)
{g : Polynomial R}
(distinguish : g.IsDistinguishedAt I)
(nmem : (PowerSeries.constantCoeff R) h ∉ I)
(eq : f = ↑g * h)
: