R : Type u
S : Type v
a b : R
n m : ℕ
inst✝² : Semiring R
p✝ q r✝ : R[X]
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
r : S
p : R[X]
i : ℕ
hi : i ∈ support (r • p)
⊢ i ∈ support p
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝² : Semiring R
p✝ q r✝ : R[X]
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
r : S
p : R[X]
⊢ support (r • p) ⊆ support p
intro i hi
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝² : Semiring R
p✝ q r✝ : R[X]
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
r : S
p : R[X]
i : ℕ
hi : ¬r • coeff p i = 0
⊢ ¬coeff p i = 0
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝² : Semiring R
p✝ q r✝ : R[X]
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
r : S
p : R[X]
i : ℕ
hi : i ∈ support (r • p)
⊢ i ∈ support p
simp [mem_support_iff] at hi⊢
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝² : Semiring R
p✝ q r✝ : R[X]
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
r : S
p : R[X]
i : ℕ
hi : coeff p i = 0
⊢ r • coeff p i = 0
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝² : Semiring R
p✝ q r✝ : R[X]
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
r : S
p : R[X]
i : ℕ
hi : ¬r • coeff p i = 0
⊢ ¬coeff p i = 0
contrapose! hi
no goals
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝² : Semiring R
p✝ q r✝ : R[X]
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
r : S
p : R[X]
i : ℕ
hi : coeff p i = 0
⊢ r • coeff p i = 0
simp [hi]