[Merged by Bors] - feat(RingTheory/Ideal/Colon): add a few API lemmas

Mathlib/RingTheory/Ideal/Colon.lean

@@ -65,8 +65,6 @@ theorem bot_colon : colon (⊥ : Submodule R M) (N : Set M) = N.annihilator := b
   ext x
   simp [mem_colon, mem_annihilator]
 
-@[deprecated (since := "2026-01-11")] alias colon_bot := bot_colon
-
 theorem colon_mono (hn : N₁ ≤ N₂) (hs : S₁ ⊆ S₂) : N₁.colon S₂ ≤ N₂.colon S₁ :=
   fun _ hrns ↦ mem_colon.mpr fun s₁ hs₁ ↦ hn <| (mem_colon).mp hrns s₁ <| hs hs₁
 
@@ -95,6 +93,11 @@ lemma inf_colon : (N₁ ⊓ N₂).colon S = N₁.colon S ⊓ N₂.colon S := by
 lemma iInf_colon {ι : Sort*} (f : ι → Submodule R M) : (⨅ i, f i).colon S = ⨅ i, (f i).colon S := by
   aesop (add simp mem_colon)
 
+@[simp]
+lemma colon_finsetInf {ι : Type*} (s : Finset ι) (f : ι → Submodule R M) :
+    (s.inf f).colon S = s.inf (fun i ↦ (f i).colon S) := by
+  aesop (add simp mem_colon)
+
 @[simp]
 lemma top_colon : (⊤ : Submodule R M).colon S = ⊤ := by
   aesop (add simp mem_colon)
@@ -111,17 +114,26 @@ lemma colon_iUnion {ι : Sort*} (f : ι → Set M) : N.colon (⋃ i, f i) = ⨅
 lemma colon_empty : N.colon (∅ : Set M) = ⊤ := by
   aesop (add simp mem_colon)
 
+lemma colon_singleton_zero : N.colon {0} = ⊤ := by
+  simp
+
+lemma colon_bot : N.colon ((⊥ : Submodule R M) : Set M) = ⊤ := by
+  simp
+
 end Semiring
 
 section CommSemiring
 
 variable [CommSemiring R] [AddCommMonoid M] [Module R M]
-variable {N : Submodule R M} {S : Set M}
+variable {N N' : Submodule R M} {S : Set M}
 
 @[deprecated mem_colon (since := "2026-01-15")]
 theorem mem_colon' {r} : r ∈ N.colon S ↔ S ≤ comap (r • (LinearMap.id : M →ₗ[R] M)) N :=
   mem_colon
 
+theorem mem_colon_iff_le {r} : r ∈ N.colon N' ↔ r • N' ≤ N := by
+  aesop (add simp SetLike.coe_subset_coe)
+
 /-- A variant for arbitrary sets in commutative semirings -/
 theorem bot_colon' : (⊥ : Submodule R M).colon S = (span R S).annihilator := by
   aesop (add simp [mem_colon, mem_annihilator_span])