feat(ring_theory/ideal/operations): annihilator_smul (#9151)

Co-authored-by: Chris Hughes <chrishughes24@gmail.com>

src/ring_theory/ideal/operations.lean

@@ -113,6 +113,15 @@ smul_mono h (le_refl N)
 theorem smul_mono_right (h : N ≤ P) : I • N ≤ I • P :=
 smul_mono (le_refl I) h
 
+@[simp] theorem annihilator_smul (N : submodule R M) : annihilator N • N = ⊥ :=
+eq_bot_iff.2 (smul_le.2 (λ r, mem_annihilator.1))
+
+@[simp] theorem annihilator_mul (I : ideal R) : annihilator I * I = ⊥ :=
+annihilator_smul I
+
+@[simp] theorem mul_annihilator (I : ideal R) : I * annihilator I = ⊥ :=
+by rw [mul_comm, annihilator_mul]
+
 variables (I J N P)
 @[simp] theorem smul_bot : I • (⊥ : submodule R M) = ⊥ :=
 eq_bot_iff.2 $ smul_le.2 $ λ r hri s hsb,