R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
i j k : ℕ
⊢ I ^ k • I ^ i • N F j ≤ I ^ k • N F (i + j)
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
i j k : ℕ
⊢ I ^ (i + k) • N F j ≤ I ^ k • N F (i + j)
rw [add_comm, pow_add, mul_smul]
no goals
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
i j k : ℕ
⊢ I ^ k • I ^ i • N F j ≤ I ^ k • N F (i + j)
exact Submodule.smul_mono_right (F.pow_smul_le i j)