case h
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
x✝ : PolynomialModule R M
⊢ x✝ ∈ Filtration.submodule (F ⊓ F') ↔ x✝ ∈ 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
⊢ Filtration.submodule (F ⊓ F') = Filtration.submodule F ⊓ Filtration.submodule F'
ext
no goals
case h
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
x✝ : PolynomialModule R M
⊢ x✝ ∈ Filtration.submodule (F ⊓ F') ↔ x✝ ∈ Filtration.submodule F ⊓ Filtration.submodule F'
exact forall_and