R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
⊢ Submodule.span { x // x ∈ reesAlgebra I } ↑(Filtration.submodule F) = Filtration.submodule F
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
⊢ Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ), ↑(single R i) '' ↑(N F i)) = Filtration.submodule F
rw [← Submodule.span_closure, submodule_closure_single, Submodule.coe_toAddSubmonoid]
no goals
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
⊢ Submodule.span { x // x ∈ reesAlgebra I } ↑(Filtration.submodule F) = Filtration.submodule F
exact Submodule.span_eq (Filtration.submodule F)