Documentation
Mathlib
.
RingTheory
.
Polynomial
.
Ideal
Search
return to top
source
Imports
Init
Mathlib.Algebra.Polynomial.RingDivision
Mathlib.RingTheory.Adjoin.Polynomial
Mathlib.RingTheory.Ideal.Maps
Imported by
Polynomial
.
mem_span_C_X_sub_C_X_sub_C_iff_eval_eval_eq_zero
Polynomial
.
ker_evalRingHom
Polynomial
.
ker_modByMonicHom
Algebra
.
mem_ideal_map_adjoin
Ideals in polynomial rings
#
source
theorem
Polynomial
.
mem_span_C_X_sub_C_X_sub_C_iff_eval_eval_eq_zero
{R :
Type
u_1}
[
CommRing
R
]
{a :
R
}
{b :
Polynomial
R
}
{P :
Polynomial
(
Polynomial
R
)
}
:
P
∈
Ideal.span
{
C
(
X
-
C
a
)
,
X
-
C
b
}
↔
eval
a
(
eval
b
P
)
=
0
source
theorem
Polynomial
.
ker_evalRingHom
{R :
Type
u_1}
[
CommRing
R
]
(x :
R
)
:
RingHom.ker
(
evalRingHom
x
)
=
Ideal.span
{
X
-
C
x
}
source
@[simp]
theorem
Polynomial
.
ker_modByMonicHom
{R :
Type
u_1}
[
CommRing
R
]
{q :
Polynomial
R
}
(hq :
q
.
Monic
)
:
LinearMap.ker
q
.
modByMonicHom
=
Submodule.restrictScalars
R
(
Ideal.span
{
q
}
)
source
theorem
Algebra
.
mem_ideal_map_adjoin
{R :
Type
u_2}
{S :
Type
u_3}
[
CommRing
R
]
[
CommRing
S
]
[
Algebra
R
S
]
(x :
S
)
(I :
Ideal
R
)
{y :
↥
(
adjoin
R
{
x
}
)
}
:
y
∈
Ideal.map
(
algebraMap
R
↥
(
adjoin
R
{
x
}
)
)
I
↔
∃ (
p
:
Polynomial
R
),
(∀ (
i
:
ℕ
),
p
.
coeff
i
∈
I
)
∧
(
Polynomial.aeval
x
)
p
=
↑
y