no goals
R : Type u
M : Type v
F : Type ?u.61436
G : Type ?u.61439
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I✝ J : Ideal R
N P : Submodule R M
I : Ideal R
⊢ I * annihilator I = ⊥
rw [mul_comm, annihilator_mul]