chore(Algebra): replace NoZeroSMulDivisors with Module.IsTorsionFree

[YaelDillies]

NoZeroSMulDivisors R M is mathematically wrong when R isn't a domain, so we replace it with the better definition Module.IsTorsionFree R M. In fact, it never holds in such case unless M is trivial.

Here's a proof that NoZeroSMulDivisors R M implies NoZeroDivisors R.
If m : M is non-zero and r s : R are such that r * s = 0, then r • s • m = (r * s) • m = 0, so by NoZeroSMulDivisors we get r = 0 ∨ s = 0 ∨ m = 0. But m ≠ 0, so r = 0 ∨ s = 0, as wanted.

This means that one can eagerly replace NoZeroSMulDivisors R M with NoZeroDivisors R + Module.IsTorsionFree R M. Doing so, some lemmas become vacuous and some instances redundant. We remove them.

Since NoZeroDivisors R is usually mathematically incorrect when R is a semiring, I in fact replace NoZeroSMulDivisors R M with IsDomain R + Module.IsTorsionFree R M.

---

• depends on: [Merged by Bors] - chore(Algebra/ModEq): don't import modules #30614
• depends on: [Merged by Bors] - chore(Algebra/Group/EvenFunction): don't import torsion-free modules #30628
• depends on: refactor(Algebra/Quaternion): intermediate Module instance #30678
• depends on: chore: use IsAddTorsionFree M instead of NoZeroSMulDivisors ℕ M/NoZeroSMulDivisors ℤ M #30683
• depends on: [Merged by Bors] - chore(Analysis/Convex/Combination): remove an unused variable #30707
• depends on: feat(Localization): r / m in the localisation is regular iff r is #30708
• depends on: feat(Algebra/Module/Torsion): more instances #30716

[github-actions]

PR summary af74401434

Import changes exceeding 2%

%	File
+6.48%	Mathlib.Algebra.GroupWithZero.NonZeroDivisors
+4.89%	Mathlib.Algebra.Module.Submodule.Basic
+116.00%	Mathlib.Algebra.NoZeroSMulDivisors.Defs
+62.33%	Mathlib.Algebra.NoZeroSMulDivisors.Pi
+119.80%	Mathlib.Algebra.NoZeroSMulDivisors.Prod
+11.52%	Mathlib.Algebra.Ring.Action.Pointwise.Finset
+70.93%	Mathlib.Algebra.Ring.Action.Pointwise.Set
+7.88%	Mathlib.Algebra.Ring.Int.Defs
+14.81%	Mathlib.Algebra.Ring.Nat
+4.63%	Mathlib.Algebra.Ring.NonZeroDivisors
+6.35%	Mathlib.GroupTheory.GroupAction.Basic

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.NoZeroSMulDivisors.Prod	202	444	+242 (+119.80%)
Mathlib.Algebra.NoZeroSMulDivisors.Defs	200	432	+232 (+116.00%)
Mathlib.Algebra.Ring.Action.Pointwise.Set	313	535	+222 (+70.93%)
Mathlib.Algebra.NoZeroSMulDivisors.Pi	292	474	+182 (+62.33%)
Mathlib.Algebra.Ring.Nat	135	155	+20 (+14.81%)
Mathlib.Algebra.Ring.Action.Pointwise.Finset	599	668	+69 (+11.52%)
Mathlib.Algebra.Ring.Int.Defs	165	178	+13 (+7.88%)
Mathlib.Algebra.GroupWithZero.NonZeroDivisors	571	608	+37 (+6.48%)
Mathlib.GroupTheory.GroupAction.Basic	614	653	+39 (+6.35%)
Mathlib.Algebra.Module.Submodule.Basic	614	644	+30 (+4.89%)
Mathlib.Algebra.Ring.NonZeroDivisors	583	610	+27 (+4.63%)
Mathlib.GroupTheory.Subgroup.Saturated	469	459	-10 (-2.13%)
Mathlib.RingTheory.LocalRing.Module	1984	1944	-40 (-2.02%)
Mathlib.Algebra.Module.LinearMap.Basic	495	503	+8 (+1.62%)
Mathlib.Algebra.Module.Basic	479	485	+6 (+1.25%)
Mathlib.Algebra.Module.TransferInstance	565	571	+6 (+1.06%)
Mathlib.RingTheory.Spectrum.Prime.FreeLocus	2083	2061	-22 (-1.06%)
Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set	487	486	-1 (-0.21%)
Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset	630	629	-1 (-0.16%)
Mathlib.LinearAlgebra.BilinearMap	689	688	-1 (-0.15%)
Mathlib.LinearAlgebra.Dual.Defs	701	700	-1 (-0.14%)
Mathlib.LinearAlgebra.Span.Basic	784	783	-1 (-0.13%)

Import changes for all files

Files	Import difference
There are 3162 files with changed transitive imports taking up over 143288 characters: this is too many to display!
You can run scripts/import_trans_difference.sh all locally to see the whole output.

---

Declarations diff

+ CharZero.of_isAddTorsionFree
+ Function.Injective.moduleIsTorsionFree
+ Ideal.iInf_pow_smul_eq_bot_of_isTorsionFree
+ IsAddTorsionFree.nsmul_eq_zero_iff'
+ IsAddTorsionFree.of_isTorsionFree
+ IsAddTorsionFree.to_isTorsionFree_nat
+ IsHausdorff.of_isTorsionFree
+ IsMulTorsionFree.pow_eq_one_iff_left
+ IsMulTorsionFree.pow_eq_one_iff_right
+ IsMulTorsionFree.zpow_eq_one_iff
+ IsMulTorsionFree.zpow_eq_one_iff_left
+ IsMulTorsionFree.zpow_eq_one_iff_right
+ IsRegular.isSMulRegular
+ IsRegular.smul_eq_zero_iff_right
+ IsRegular.smul_ne_zero_iff_right
+ IsRegular.smul_right_inj
+ IsRegular.smul_right_injective
+ IsSMulRegular.of_ne_zero
+ IsTorsionFree.trans_faithfulSMul
+ Module.IsTorsionFree
+ Module.IsTorsionFree.of_smul_eq_zero
+ Module.isTorsionFree_iff_smul_eq_zero
+ Module.isTorsionFree_int_iff_isAddTorsionFree
+ Module.isTorsionFree_nat_iff_isAddTorsionFree
+ Semifield.to_moduleIsTorsionFree
+ _root_.Module.IsTorsionFree.of_isLocalization
+ addEquivTuple
+ coe_addEquivTuple
+ coe_symm_addEquivTuple
+ exists_mk'_eq
+ instIsTorsionFreeInteger
+ instModuleIsTorsionFree'
+ instance (f : K[X]) : Module.IsTorsionFree K f.SplittingField
+ instance (priority := 100) : Module.IsTorsionFree R M
+ instance (priority := 100) IsAddTorsionFree.of_isDomain_charZero : IsAddTorsionFree R
+ instance (priority := 100) NNRatModule.to_isAddTorsionFree [AddCommMonoid M] [Module ℚ≥0 M] :
+ instance (priority := 100) RatModule.to_isAddTorsionFree [AddCommGroup M] [Module ℚ M] :
+ instance (priority := 100) moduleIsTorsionFree [NoZeroDivisors R] : Module.IsTorsionFree R M
+ instance (α : Type*) [TopologicalSpace α] : IsAddTorsionFree (LocallyConstant α ℤ)
+ instance : Add ℍ[R,c₁,c₂,c₃] := fast_instance% (equivProd c₁ c₂ c₃).add
+ instance : Module.IsTorsionFree (CyclotomicRing n A K) (CyclotomicField n K)
+ instance : Module.IsTorsionFree (𝓞 K) (𝓞 L)
+ instance : Module.IsTorsionFree (𝓞 K) K
+ instance : Module.IsTorsionFree (𝓞 K) L
+ instance : Module.IsTorsionFree R (v.adicCompletionIntegers K)
+ instance : Module.IsTorsionFree R Sₚ := by
+ instance : Module.IsTorsionFree S Sₚ := by
+ instance : Neg ℍ[R,c₁,c₂,c₃] := fast_instance% (equivProd c₁ c₂ c₃).Neg
+ instance : SMul S ℍ[R,c₁,c₂,c₃] := fast_instance% (equivProd ..).smul _
+ instance : Sub ℍ[R,c₁,c₂,c₃] := fast_instance% (equivProd c₁ c₂ c₃).sub
+ instance : Zero ℍ[R,c₁,c₂,c₃] := fast_instance% (equivProd c₁ c₂ c₃).zero
+ instance [IsDomain R] (S : Submonoid R) [IsTorsionFree R M] :
+ instance [IsFractionRing A K] : Module.IsTorsionFree A (CyclotomicField n K) := by
+ instance [Module.IsTorsionFree R M] : Module.IsTorsionFree R N
+ instance [Module.IsTorsionFree S M'] : Module.IsTorsionFree S (M →ₛₗ[σ₁₂] M')
+ instance [Module.IsTorsionFree S M₂] : Module.IsTorsionFree S (MultilinearMap R M₁ M₂)
+ instance [Module.IsTorsionFree S T] : Module.IsTorsionFree Sₚ Tₚ
+ instance [Module.IsTorsionFree S T] [Algebra.IsSeparable L F] :
+ instance [Monoid S] [MulAction S R] : MulAction S ℍ[R,c₁,c₂,c₃]
+ instance [Monoid S] [MulAction S R] : MulAction S ℍ[R]
+ instance [Nontrivial A] [IsTorsionFree R A] : FaithfulSMul R A
+ instance [SMulCommClass S T R] : SMulCommClass S T ℍ[R,c₁,c₂,c₃] := (equivTuple ..).smulCommClass ..
+ instance [Semiring R] [IsDomain R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] :
+ instance [Semiring S] [AddCommGroup R] [DistribMulAction S R] : DistribMulAction S ℍ[R,c₁,c₂,c₃]
+ instance [Semiring S] [AddCommGroup R] [Module S R] : Module S ℍ[R,c₁,c₂,c₃]
+ instance [Semiring S] [DistribMulAction S R] : DistribMulAction S ℍ[R]
+ instance [Semiring S] [Module S R] : Module S ℍ[R]
+ instance [Semiring S] [Module S R] [Module.IsTorsionFree S R] :
+ instance _root_.Function.noZeroSMulDivisors {ι α β : Type*} [Semiring α] [IsDomain α]
+ instance {R S : Type*} [CommRing R] [IsDomain R] {P : Ideal R} [CommRing S] [Algebra R S]
+ instance {S : Type*} [Semiring S] [Module S R] [Module.IsTorsionFree S R] :
+ isLeftRegular_iff_isRegular
+ isRegular_mk'
+ isRightRegular_iff_isRegular
+ isTorsionFree
+ isTorsionFree_of_forall_isRegular
+ mk_eq_zero
+ mk_smul_mk
+ smul_left_inj
+ toSubsemigroup_inj
+ toSubsemigroup_injective
++ instIsDomain
++ mk_eq_bot
+++ instIsTorsionFree
+++ instModuleIsTorsionFree
+++++++++ moduleIsTorsionFree
++-- aeval_algebraMap_eq_zero_iff
++-- ext
++-- lsmul_injective
++-- mk'
++-- nonTorsionWeight_of
+-+- smul_eq_zero
+-+- support_smul_eq
- CharZero.of_noZeroSMulDivisors
- Ideal.iInf_pow_smul_eq_bot_of_noZeroSMulDivisors
- IsAddTorsionFree.of_noZeroSMulDivisors_int
- IsAddTorsionFree.of_noZeroSMulDivisors_nat
- IsHausdorff.of_noZeroSMulDivisors
- IsTorsion.not_torsion_free
- IsTorsionFree.noZeroSMulDivisors_int
- IsTorsionFree.noZeroSMulDivisors_nat
- IsTorsionFree.not_torsion
- IsTorsionFree.of_noZeroSMulDivisors
- IsTorsionFree.prod
- IsTorsionFree.quotient_torsion
- IsTorsionFree.subgroup
- Nat.noZeroSMulDivisors
- NoZeroSMulDivisors.int_of_charZero
- NoZeroSMulDivisors.trans_faithfulSMul
- _root_.NoZeroSMulDivisors_of_isLocalization
- instNoZeroSMulDivisorsInteger
- instance (S : Submonoid R) [NoZeroSMulDivisors R M] :
- instance (f : K[X]) : NoZeroSMulDivisors K f.SplittingField
- instance (priority := 100) NNRatModule.noZeroSMulDivisors [AddCommMonoid M] [Module ℚ≥0 M] :
- instance (priority := 100) RatModule.noZeroSMulDivisors [AddCommGroup M] [Module ℚ M] :
- instance (priority := 100) [IsDomain R] : NoZeroSMulDivisors R M := by
- instance (priority := 100) noZeroSMulDivisors [NoZeroDivisors R] : NoZeroSMulDivisors R M
- instance (α : Type*) [TopologicalSpace α] : NoZeroSMulDivisors ℤ (LocallyConstant α ℤ) := by
- instance : Add ℍ[R,c₁,c₂,c₃]
- instance : Neg ℍ[R,c₁,c₂,c₃] := ⟨fun a => ⟨-a.1, -a.2, -a.3, -a.4⟩⟩
- instance : NoZeroSMulDivisors (CyclotomicRing n A K) (CyclotomicField n K)
- instance : NoZeroSMulDivisors (𝓞 K) (𝓞 L)
- instance : NoZeroSMulDivisors (𝓞 K) K
- instance : NoZeroSMulDivisors (𝓞 K) L
- instance : NoZeroSMulDivisors R (v.adicCompletionIntegers K)
- instance : NoZeroSMulDivisors R Sₚ := by
- instance : NoZeroSMulDivisors S Sₚ := by
- instance : SMul S ℍ[R,c₁,c₂,c₃] where smul s a := ⟨s • a.1, s • a.2, s • a.3, s • a.4⟩
- instance : Sub ℍ[R,c₁,c₂,c₃]
- instance : Zero ℍ[R,c₁,c₂,c₃] := ⟨⟨0, 0, 0, 0⟩⟩
- instance [AddCommGroup M] [NoZeroSMulDivisors ℤ M] : NoZeroSMulDivisors ℕ M
- instance [IsAddTorsionFree M] : IsTorsionFree ℕ M
- instance [IsFractionRing A K] : NoZeroSMulDivisors A (CyclotomicField n K) := by
- instance [NoZeroDivisors R] : NoZeroSMulDivisors R ℍ[R,c₁,c₂,c₃] := ⟨by
- instance [NoZeroSMulDivisors R M] : NoZeroSMulDivisors R N
- instance [NoZeroSMulDivisors S M'] : NoZeroSMulDivisors S (M →ₛₗ[σ₁₂] M')
- instance [NoZeroSMulDivisors S M₂] : NoZeroSMulDivisors S (MultilinearMap R M₁ M₂)
- instance [NoZeroSMulDivisors S T] : NoZeroSMulDivisors Sₚ Tₚ
- instance [NoZeroSMulDivisors S T] [Algebra.IsSeparable L F] :
- instance [NoZeroSMulDivisors ℤ M] : NoZeroSMulDivisors ℕ M
- instance [Nontrivial A] [NoZeroSMulDivisors R A] : FaithfulSMul R A
- instance [SMulCommClass S T R] : SMulCommClass S T ℍ[R,c₁,c₂,c₃]
- instance [Zero S] [SMulWithZero S R] [NoZeroSMulDivisors S R] :
- instance _root_.Function.noZeroSMulDivisors {ι α β : Type*} [Zero α] [Zero β]
- instance {R S : Type*} [CommRing R] [NoZeroDivisors R] {P : Ideal R} [CommRing S] [Algebra R S]
- instance {S : Type*} [Zero S] [SMulZeroClass S R] [NoZeroSMulDivisors S R] :
- isTorsionFree_iff_noZeroSMulDivisors_int
- isTorsionFree_iff_noZeroSMulDivisors_nat
- isTorsionFree_of_subsingleton
- noZeroSMulDivisors_finset
- noZeroSMulDivisors_iff_torsion_eq_bot
- noZeroSMulDivisors_int_iff_isAddTorsionFree
- noZeroSMulDivisors_nat_iff_isAddTorsionFree
- noZeroSMulDivisors_set
- noZeroSMulDivisors_top
- not_isTorsionFree_iff
-++- linearIndependent_single_of_ne_zero
-- IsTorsionFree
--+------+-- noZeroSMulDivisors
--- noZeroSMulDivisors_bot
---- instNoZeroSMulDivisors

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

Decrease in tech debt: (relative, absolute) = (1.00, 0.02)

Current number	Change	Type
57	-1	disabled deprecation lints

Current commit b839c18416
Reference commit af74401434

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

---

note: file Mathlib/Algebra/Module/Torsion.lean` was renamed to `Mathlib/Algebra/Module/Torsion/Basic.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - chore(Algebra/ModEq): don't import modules #30614
• [Merged by Bors] - chore(Algebra/Group/EvenFunction): don't import torsion-free modules #30628
• refactor(Algebra/Quaternion): intermediate Module instance #30678
• chore: use IsAddTorsionFree M instead of NoZeroSMulDivisors ℕ M/NoZeroSMulDivisors ℤ M #30683
• [Merged by Bors] - chore(Analysis/Convex/Combination): remove an unused variable #30707
• feat(Localization): r / m in the localisation is regular iff r is #30708
• feat(Algebra/Module/Torsion): more instances #30716
  By Dependent Issues (🤖). Happy coding!

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.