chore(Algebra): deprecate a few more NoZeroSMulDivisors lemmas (leanprover-community#34203)

These were forgotten in leanprover-community#33873.

Author: YaelDillies

Mathlib/Algebra/Algebra/Basic.lean

@@ -364,34 +364,6 @@ instance (R : Type*) [Ring R] [CharZero R] : FaithfulSMul ℤ R := by
 
 end FaithfulSMul
 
-namespace NoZeroSMulDivisors
-
--- see Note [lower instance priority]
-instance (priority := 100) instOfFaithfulSMul {R A : Type*}
-    [CommSemiring R] [Nontrivial R] [Ring A] [Algebra R A] [NoZeroDivisors A] [FaithfulSMul R A] :
-    IsTorsionFree R A where
-  isSMulRegular r hr a b hab := by
-    rw [← sub_eq_zero, ← smul_sub] at hab
-    simpa [Algebra.smul_def, FaithfulSMul.algebraMap_eq_zero_iff, sub_eq_zero, hr.ne_zero] using hab
-
-variable {R A : Type*} [CommRing R] [IsDomain R] [Ring A] [Algebra R A]
-
-instance [Nontrivial A] [IsTorsionFree R A] : FaithfulSMul R A where
-  eq_of_smul_eq_smul {r₁ r₂} h := by
-    specialize h 1
-    rw [← sub_eq_zero, ← sub_smul, smul_eq_zero, sub_eq_zero] at h
-    exact h.resolve_right one_ne_zero
-
-lemma iff_faithfulSMul [IsDomain A] : IsTorsionFree R A ↔ FaithfulSMul R A where
-  mp _ := inferInstance
-  mpr _ := inferInstance
-
-theorem iff_algebraMap_injective [IsDomain A] :
-    IsTorsionFree R A ↔ Injective (algebraMap R A) := by
-  rw [iff_faithfulSMul, faithfulSMul_iff_algebraMap_injective]
-
-end NoZeroSMulDivisors
-
 section IsScalarTower
 
 variable {R : Type*} [CommSemiring R]
@@ -457,32 +429,39 @@ lemma Module.IsTorsionFree.of_faithfulSMul [Semiring S] [Module S R] [Module S A
   (FaithfulSMul.algebraMap_injective R A).moduleIsTorsionFree _
     (by simp [Algebra.algebraMap_eq_smul_one])
 
-lemma Module.IsTorsionFree.trans_faithfulSMul [Nontrivial R] [IsDomain A] [AddCommMonoid M]
+lemma Module.IsTorsionFree.trans_faithfulSMul [Nontrivial R] [IsCancelMulZero A] [AddCommMonoid M]
     [Module A M] [Module R M] [IsTorsionFree A M] [IsScalarTower R A M] : IsTorsionFree R M :=
-  .comap (algebraMap R A) (fun r hr ↦ by simpa [isRegular_iff_ne_zero] using hr.ne_zero) (by simp)
+  .comap (algebraMap R A) (fun r hr ↦ .of_ne_zero <| by simpa using hr.ne_zero) (by simp)
 
 -- see Note [lower instance priority]
-instance (priority := 100) FaithfulSMul.to_isTorsionFree [Nontrivial R] [IsDomain A] :
+instance (priority := 100) FaithfulSMul.to_isTorsionFree [Nontrivial R] [IsCancelMulZero A] :
     IsTorsionFree R A := .trans_faithfulSMul R A A
 
 end FaithfulSMul
 
 namespace Module
 variable {R A : Type*} [CommRing R] [IsDomain R] [Ring A] [Algebra R A]
 
-instance (priority := 100) IsTorsionFree.to_faithfulSMul [Nontrivial A] [IsTorsionFree R A] :
-    FaithfulSMul R A where
+instance IsTorsionFree.to_faithfulSMul [IsCancelMulZero R] [Nontrivial A]
+    [IsTorsionFree R A] : FaithfulSMul R A where
   eq_of_smul_eq_smul h := smul_left_injective _ one_ne_zero <| h 1
 
-lemma isTorsionFree_iff_faithfulSMul [IsDomain A] : IsTorsionFree R A ↔ FaithfulSMul R A :=
+variable [IsDomain A]
+
+lemma isTorsionFree_iff_faithfulSMul : IsTorsionFree R A ↔ FaithfulSMul R A :=
   ⟨fun _ ↦ inferInstance, fun _ ↦ inferInstance⟩
 
-lemma isTorsionFree_iff_algebraMap_injective [IsDomain A] :
-    IsTorsionFree R A ↔ Injective (algebraMap R A) := by
+lemma isTorsionFree_iff_algebraMap_injective : IsTorsionFree R A ↔ Injective (algebraMap R A) := by
   rw [isTorsionFree_iff_faithfulSMul, faithfulSMul_iff_algebraMap_injective]
 
 end Module
 
+@[deprecated (since := "2026-01-21")]
+alias NoZeroSMulDivisors.iff_algebraMap_injective := isTorsionFree_iff_algebraMap_injective
+
+@[deprecated (since := "2026-01-21")]
+alias NoZeroSMulDivisors.iff_faithfulSMul := isTorsionFree_iff_faithfulSMul
+
 /-! TODO: The following lemmas no longer involve `Algebra` at all, and could be moved closer
 to `Algebra/Module/Submodule.lean`. Currently this is tricky because `ker`, `range`, `⊤`, and `⊥`
 are all defined in `LinearAlgebra/Basic.lean`. -/

Mathlib/Algebra/Module/Torsion/Free.lean

@@ -91,7 +91,7 @@ lemma Module.IsTorsionFree.trans [Module S R] [IsTorsionFree S R] [IsScalarTower
     exact ⟨fun x y hxy ↦ hs.isSMulRegular <| by simpa using hxy,
       fun x y hxy ↦ hs.isSMulRegular <| by simpa using hxy⟩
 
-variable [IsDomain R]
+variable [IsCancelMulZero R]
 
 lemma IsSMulRegular.of_ne_zero (hr : r ≠ 0) : IsSMulRegular M r :=
   (IsRegular.of_ne_zero hr).isSMulRegular
@@ -160,14 +160,12 @@ lemma Module.IsTorsionFree.of_smul_eq_zero [Nontrivial R]
   isSMulRegular r hr m₁ m₂ hm := by
     simpa [sub_eq_zero, hr.ne_zero] using h r (m₁ - m₂) (by simpa [smul_sub, sub_eq_zero] using hm)
 
-variable [IsDomain R]
-
-lemma Module.isTorsionFree_iff_smul_eq_zero :
+lemma Module.isTorsionFree_iff_smul_eq_zero [IsDomain R] :
     IsTorsionFree R M ↔ ∀ (r : R) (m : M), r • m = 0 → r = 0 ∨ m = 0 where
   mp _ _ _ := smul_eq_zero.1
   mpr := .of_smul_eq_zero
 
-variable [IsTorsionFree R M]
+variable [IsCancelMulZero R] [IsTorsionFree R M]
 
 variable (R) in
 lemma smul_left_injective (hm : m ≠ 0) : ((· • m) : R → M).Injective := by

Mathlib/RingTheory/Extension/Generators.lean

@@ -574,14 +574,18 @@ lemma ker_naive {σ : Type*} {I : Ideal (MvPolynomial σ R)}
     (Generators.naive s hs).ker = I :=
   I.mk_ker
 
-@[simp]
+-- FIXME: `simpNF` times out synthesizing
+-- `FaithfulSMul (Algebra.Generators.ofAlgHom f h).toExtension.Ring S`.
+@[simp, nolint simpNF]
 lemma ker_ofAlgHom {I : Type*} (f : MvPolynomial I R →ₐ[R] S) (h : Function.Surjective ⇑f) :
     (ofAlgHom f h).ker = RingHom.ker f.toRingHom := by
   change RingHom.ker _ = _
   congr
   exact MvPolynomial.ringHom_ext (by simp) (by simp [ofAlgHom])
 
-@[simp]
+-- FIXME: `simpNF` times out synthesizing
+-- `FaithfulSMul (P.ofAlgEquiv e).toExtension.Ring T`.
+@[simp, nolint simpNF]
 lemma ker_ofAlgEquiv (P : Generators R S ι) {T : Type*} [CommRing T] [Algebra R T] (e : S ≃ₐ[R] T) :
     (P.ofAlgEquiv e).ker = P.ker := by
   rw [ker_eq_ker_aeval_val, ofAlgEquiv_val, Function.comp_def, ← AlgHom.coe_coe,