no goals
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
i : ℕ
⊢ ↑(I ^ i • ⊤) = ↑((fun i => toAddSubgroup (I ^ i • ⊤)) i)
simp
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
i : ℕ
a : R
a_in : a ∈ I ^ i
⊢ a ∈ (fun x => x • m) ⁻¹' ↑(I ^ i • ⊤)
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
i : ℕ
a : R
a_in : a ∈ ↑(I ^ i • ⊤)
⊢ a ∈ (fun x => x • m) ⁻¹' ↑(I ^ i • ⊤)
replace a_in : a ∈ I ^ i := by simpa [(I ^ i).mul_top] using a_in
no goals
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
i : ℕ
a : R
a_in : a ∈ I ^ i
⊢ a ∈ (fun x => x • m) ⁻¹' ↑(I ^ i • ⊤)
exact smul_mem_smul a_in mem_top
no goals
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
i : ℕ
a : R
a_in : a ∈ ↑(I ^ i • ⊤)
⊢ a ∈ I ^ i
simpa [(I ^ i).mul_top] using a_in