R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I✝ : Ideal R
F F' : Filtration I✝ M
I : Ideal R
N : Submodule R M
⊢ ∀ (n : ℕ), n ≥ 0 → I • Ideal.Filtration.N (stableFiltration I N) n = Ideal.Filtration.N (stableFiltration I N) (n + 1)
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I✝ : Ideal R
F F' : Filtration I✝ M
I : Ideal R
N : Submodule R M
⊢ Stable (stableFiltration I N)
use 0
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I✝ : Ideal R
F F' : Filtration I✝ M
I : Ideal R
N : Submodule R M
n : ℕ
a✝ : n ≥ 0
⊢ I • Ideal.Filtration.N (stableFiltration I N) n = Ideal.Filtration.N (stableFiltration I N) (n + 1)
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I✝ : Ideal R
F F' : Filtration I✝ M
I : Ideal R
N : Submodule R M
⊢ ∀ (n : ℕ), n ≥ 0 → I • Ideal.Filtration.N (stableFiltration I N) n = Ideal.Filtration.N (stableFiltration I N) (n + 1)
intro n _
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I✝ : Ideal R
F F' : Filtration I✝ M
I : Ideal R
N : Submodule R M
n : ℕ
a✝ : n ≥ 0
⊢ I • I ^ n • N = I ^ (n + 1) • N
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I✝ : Ideal R
F F' : Filtration I✝ M
I : Ideal R
N : Submodule R M
n : ℕ
a✝ : n ≥ 0
⊢ I • Ideal.Filtration.N (stableFiltration I N) n = Ideal.Filtration.N (stableFiltration I N) (n + 1)
dsimp
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 : Ideal R
N : Submodule R M
n : ℕ
a✝ : n ≥ 0
⊢ I • I ^ n • N = I ^ (n + 1) • N
rw [add_comm, pow_add, mul_smul, pow_one]