R : Type u
S : Type ?u.952181
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
⊢ ∑ v in support p, ↑(monomial v) (coeff v p) ∈ I
R : Type u
S : Type ?u.952181
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
⊢ p ∈ I
rw [as_sum p]
R : Type u
S : Type ?u.952181
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
⊢ ∀ (m : σ →₀ ℕ), m ∈ support p → ↑(monomial m) (coeff m p) ∈ I
R : Type u
S : Type ?u.952181
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
⊢ ∑ v in support p, ↑(monomial v) (coeff v p) ∈ I
suffices ∀ m ∈ p.support, monomial m (MvPolynomial.coeff m p) ∈ I by
  exact Submodule.sum_mem I this
R : Type u
S : Type ?u.952181
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
m : σ →₀ ℕ
a✝ : m ∈ support p
⊢ ↑(monomial m) (coeff m p) ∈ I
R : Type u
S : Type ?u.952181
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
⊢ ∀ (m : σ →₀ ℕ), m ∈ support p → ↑(monomial m) (coeff m p) ∈ I
intro m _
R : Type u
S : Type ?u.952181
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
m : σ →₀ ℕ
a✝ : m ∈ support p
⊢ ↑C (coeff m p) * ↑(monomial m) 1 ∈ I
R : Type u
S : Type ?u.952181
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
m : σ →₀ ℕ
a✝ : m ∈ support p
⊢ ↑(monomial m) (coeff m p) ∈ I
rw [← mul_one (coeff m p), ← C_mul_monomial]
R : Type u
S : Type ?u.952181
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
m : σ →₀ ℕ
a✝ : m ∈ support p
⊢ ↑C (coeff m p) ∈ I
R : Type u
S : Type ?u.952181
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
m : σ →₀ ℕ
a✝ : m ∈ support p
⊢ ↑C (coeff m p) * ↑(monomial m) 1 ∈ I
suffices C (coeff m p) ∈ I by exact I.mul_mem_right (monomial m 1) this
no goals
R : Type u
S : Type ?u.952181
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
m : σ →₀ ℕ
a✝ : m ∈ support p
⊢ ↑C (coeff m p) ∈ I
simpa [Ideal.mem_comap] using hcoe m
no goals
R : Type u
S : Type ?u.952181
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
this : ∀ (m : σ →₀ ℕ), m ∈ support p → ↑(monomial m) (coeff m p) ∈ I
⊢ ∑ v in support p, ↑(monomial v) (coeff v p) ∈ I
exact Submodule.sum_mem I this
no goals
R : Type u
S : Type ?u.952181
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
m : σ →₀ ℕ
a✝ : m ∈ support p
this : ↑C (coeff m p) ∈ I
⊢ ↑C (coeff m p) * ↑(monomial m) 1 ∈ I
exact I.mul_mem_right (monomial m 1) this