Eisenstein binomials #
For an ideal 𝓟 of a commutative ring, X ^ n - C ϖ is Eisenstein at 𝓟 when
n is positive and ϖ lies in 𝓟 but not in 𝓟 ^ 2.
Main results #
TauCeti.isEisensteinAt_X_pow_sub_Cconstructs Eisenstein binomials from ideal membership.
theorem
TauCeti.isEisensteinAt_X_pow_sub_C
{R : Type u_1}
[CommRing R]
{𝓟 : Ideal R}
{ϖ : R}
(hmem : ϖ ∈ 𝓟)
(hnotmem : ϖ ∉ 𝓟 ^ 2)
{n : ℕ}
(hn : 0 < n)
:
(Polynomial.X ^ n - Polynomial.C ϖ).IsEisensteinAt 𝓟
X ^ n - C ϖ is Eisenstein at an ideal 𝓟 when ϖ ∈ 𝓟 but ϖ ∉ 𝓟 ^ 2,
for positive n.