R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
I : Ideal R[X]
cf : ∀ (i : ℕ), ↑C (coeff f i) ∈ I
⊢ Ideal.span {g | ∃ i, ↑C (coeff f i) = g} ≤ I
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
I : Ideal R[X]
cf : ∀ (i : ℕ), ↑C (coeff f i) ∈ I
⊢ Ideal.span {g | ∃ i, g = ↑C (coeff f i)} ≤ I
simp (config := { singlePass := true }) only [@eq_comm _ _ (C _)]
no goals
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
I : Ideal R[X]
cf : ∀ (i : ℕ), ↑C (coeff f i) ∈ I
⊢ Ideal.span {g | ∃ i, ↑C (coeff f i) = g} ≤ I
exact (Ideal.span_le.trans range_subset_iff).mpr cf