case h
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
f : R[X]
⊢ ∀ (a : ℕ), coeff f a ∈ I ^ a ↔ a ∈ support f → coeff f a ∈ I ^ a
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
f : R[X]
⊢ f ∈ reesAlgebra I ↔ ∀ (i : ℕ), i ∈ support f → coeff f i ∈ I ^ i
apply forall_congr'
case h
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
f : R[X]
a : ℕ
⊢ coeff f a ∈ I ^ a ↔ a ∈ support f → coeff f a ∈ I ^ a
case h
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
f : R[X]
⊢ ∀ (a : ℕ), coeff f a ∈ I ^ a ↔ a ∈ support f → coeff f a ∈ I ^ a
intro a
case h
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
f : R[X]
a : ℕ
⊢ coeff f a = 0 → coeff f a ∈ I ^ a
case h
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
f : R[X]
a : ℕ
⊢ coeff f a ∈ I ^ a ↔ a ∈ support f → coeff f a ∈ I ^ a
rw [mem_support_iff, Iff.comm, imp_iff_right_iff, Ne.def, ← imp_iff_not_or]
no goals
case h
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
f : R[X]
a : ℕ
⊢ coeff f a = 0 → coeff f a ∈ I ^ a
exact fun e => e.symm ▸ (I ^ a).zero_mem