R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
x : ℕ
⊢ x ∈ support (map f p) → x ∈ support p
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
⊢ support (map f p) ⊆ support p
intro x
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
x : ℕ
⊢ ¬x ∈ support p → ¬x ∈ support (map f p)
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
x : ℕ
⊢ x ∈ support (map f p) → x ∈ support p
contrapose!
no goals
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
x : ℕ
⊢ ¬x ∈ support p → ¬x ∈ support (map f p)
simp (config := { contextual := true })