[Merged by Bors] - chore(Algebra): replace NoZeroSMulDivisors with Module.IsTorsionFree wlog

[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 whenever they are equivalent.

In fact, if M is non-trivial, NoZeroSMulDivisors R M implies NoZeroDivisors R:
Take m : M is non-zero. Assume 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 justifies replacing [Ring R] [Nontrivial M] [NoZeroSMulDivisors R M] with [Ring R] [IsDomain R] [Nontrivial M] [IsTorsionFree R M].

Doing so, some lemmas become vacuous and some instances redundant. We remove them.

---

• 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: [Merged by Bors] - refactor(Algebra/Quaternion): intermediate Module instance #30678
• depends on: [Merged by Bors] - 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: [Merged by Bors] - feat(Localization): r / m in the localisation is regular iff r is #30708
• depends on: [Merged by Bors] - feat(Algebra/Module/Torsion): more instances #30716
• depends on: [Merged by Bors] - chore(Algebra): move CharZero.of_module earlier #32834
• depends on: [Merged by Bors] - feat(Algebra): characterise when a submodule constructor is equal to ⊥ #32836
• depends on: [Merged by Bors] - feat(Algebra): localising a torsion-free module at regular elements #32838
• depends on: [Merged by Bors] - chore(GroupTheory/Torsion): delete deprecated declarations #32843
• depends on: [Merged by Bors] - feat(RingTheory): no extension is algebraic over the zero ring #33540
• depends on: [Merged by Bors] - chore(LinearAlgebra): make one more argument implicit in ker_toSpanSingleton #33544
• depends on: [Merged by Bors] - feat: a non-domain cannot act faithfully on a domain #33552
• depends on: [Merged by Bors] - feat(Algebra): more Module.IsTorsionFree API #33871

[github-actions]

PR summary 953704ae86

Import changes exceeding 2%

%	File
+8.41%	Mathlib.GroupTheory.GroupAction.Basic

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.GroupTheory.GroupAction.Basic	523	567	+44 (+8.41%)
Mathlib.Algebra.Order.Module.Defs	390	397	+7 (+1.79%)
Mathlib.Algebra.BigOperators.Finprod	593	600	+7 (+1.18%)
Mathlib.Algebra.Module.BigOperators	619	626	+7 (+1.13%)
Mathlib.Algebra.Order.BigOperators.Expect	766	772	+6 (+0.78%)
Mathlib.LinearAlgebra.Matrix.SemiringInverse	722	727	+5 (+0.69%)
Mathlib.Algebra.Algebra.Tower	765	770	+5 (+0.65%)
Mathlib.LinearAlgebra.LinearPMap	768	772	+4 (+0.52%)
Mathlib.RingTheory.Nilpotent.Basic	805	809	+4 (+0.50%)
Mathlib.LinearAlgebra.BilinearMap	617	614	-3 (-0.49%)
Mathlib.LinearAlgebra.Multilinear.Basic	834	838	+4 (+0.48%)
Mathlib.LinearAlgebra.Dual.Defs	627	624	-3 (-0.48%)
Mathlib.LinearAlgebra.Span.Basic	712	714	+2 (+0.28%)
Mathlib.LinearAlgebra.Alternating.Basic	941	943	+2 (+0.21%)
Mathlib.LinearAlgebra.Matrix.Basis	1221	1223	+2 (+0.16%)
Mathlib.Algebra.Module.Card	672	673	+1 (+0.15%)
Mathlib.LinearAlgebra.PerfectPairing.Restrict	1450	1452	+2 (+0.14%)
Mathlib.RingTheory.IntegralClosure.Algebra.Basic	1488	1490	+2 (+0.13%)
Mathlib.LinearAlgebra.Eigenspace.Minpoly	1506	1508	+2 (+0.13%)
Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic	1522	1524	+2 (+0.13%)
Mathlib.RingTheory.Algebraic.Integral	1535	1537	+2 (+0.13%)
Mathlib.RingTheory.Localization.Integral	1536	1538	+2 (+0.13%)
Mathlib.LinearAlgebra.RootSystem.IsValuedIn	1538	1540	+2 (+0.13%)
Mathlib.LinearAlgebra.RootSystem.Reduced	1539	1541	+2 (+0.13%)
Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear	1543	1545	+2 (+0.13%)
Mathlib.RingTheory.Conductor	1547	1549	+2 (+0.13%)
Mathlib.RingTheory.AdjoinRoot	1549	1551	+2 (+0.13%)
Mathlib.RingTheory.Ideal.GoingUp	1554	1556	+2 (+0.13%)
Mathlib.RingTheory.IntegralClosure.IntegrallyClosed	1555	1557	+2 (+0.13%)
Mathlib.RingTheory.DedekindDomain.Basic	1561	1563	+2 (+0.13%)
Mathlib.FieldTheory.SplittingField.Construction	1576	1578	+2 (+0.13%)
Mathlib.RingTheory.Valuation.LocalSubring	1579	1581	+2 (+0.13%)
Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas	1588	1590	+2 (+0.13%)
Mathlib.RingTheory.FractionalIdeal.Extended	1589	1591	+2 (+0.13%)
Mathlib.FieldTheory.Minpoly.IsConjRoot	1593	1595	+2 (+0.13%)
Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate	1595	1597	+2 (+0.13%)
Mathlib.LinearAlgebra.RootSystem.Basic	1596	1598	+2 (+0.13%)
Mathlib.LinearAlgebra.RootSystem.Hom	1597	1599	+2 (+0.13%)
Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed	1598	1600	+2 (+0.13%)
Mathlib.RingTheory.IsAdjoinRoot	1599	1601	+2 (+0.13%)
Mathlib.LinearAlgebra.RootSystem.Irreducible	1602	1604	+2 (+0.12%)
Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas	1605	1607	+2 (+0.12%)
Mathlib.LinearAlgebra.RootSystem.Chain	1610	1612	+2 (+0.12%)
Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas	1613	1615	+2 (+0.12%)
Mathlib.NumberTheory.KummerDedekind	1634	1636	+2 (+0.12%)
Mathlib.Analysis.Analytic.OfScalars	1635	1637	+2 (+0.12%)
Mathlib.FieldTheory.IsAlgClosed.Basic	1638	1640	+2 (+0.12%)
Mathlib.LinearAlgebra.Eigenspace.Pi	1652	1654	+2 (+0.12%)
Mathlib.LinearAlgebra.Basis.Basic	832	833	+1 (+0.12%)
Mathlib.LinearAlgebra.FreeModule.Basic	841	842	+1 (+0.12%)
Mathlib.Algebra.Module.LocalizedModule.Basic	846	847	+1 (+0.12%)
Mathlib.FieldTheory.PurelyInseparable.Basic	1693	1695	+2 (+0.12%)
Mathlib.Analysis.Analytic.IsolatedZeros	1704	1706	+2 (+0.12%)
Mathlib.LinearAlgebra.AffineSpace.AffineMap	860	861	+1 (+0.12%)
Mathlib.LinearAlgebra.Basis.Submodule	863	864	+1 (+0.12%)
Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic	864	865	+1 (+0.12%)
Mathlib.LinearAlgebra.AffineSpace.Pointwise	865	866	+1 (+0.12%)
Mathlib.Algebra.Lie.Weights.Basic	1733	1735	+2 (+0.12%)
Mathlib.Algebra.Lie.Weights.Linear	1734	1736	+2 (+0.12%)
Mathlib.RingTheory.AlgebraTower	867	868	+1 (+0.12%)
Mathlib.RingTheory.DedekindDomain.IntegralClosure	1737	1739	+2 (+0.12%)
Mathlib.RingTheory.NormalClosure	1738	1740	+2 (+0.12%)
Mathlib.NumberTheory.NumberField.Basic	1740	1742	+2 (+0.11%)
Mathlib.Algebra.Lie.Weights.Chain	1744	1746	+2 (+0.11%)
Mathlib.Algebra.Lie.TraceForm	1749	1751	+2 (+0.11%)
Mathlib.Algebra.Lie.Weights.Killing	1782	1784	+2 (+0.11%)
Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations	1788	1790	+2 (+0.11%)
Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple	1792	1794	+2 (+0.11%)
Mathlib.LinearAlgebra.LinearIndependent.Lemmas	913	914	+1 (+0.11%)
Mathlib.Algebra.Central.Basic	915	916	+1 (+0.11%)
Mathlib.RingTheory.DedekindDomain.PID	1833	1835	+2 (+0.11%)
Mathlib.LinearAlgebra.SesquilinearForm.Basic	917	918	+1 (+0.11%)
Mathlib.RingTheory.DedekindDomain.Instances	1844	1846	+2 (+0.11%)
Mathlib.LinearAlgebra.DFinsupp	923	924	+1 (+0.11%)
Mathlib.LinearAlgebra.Ray	926	927	+1 (+0.11%)
Mathlib.RingTheory.IntegralClosure.IntegralRestrict	1912	1914	+2 (+0.10%)
Mathlib.RingTheory.Invariant.Basic	1914	1916	+2 (+0.10%)
Mathlib.RingTheory.MvPolynomial.Tower	957	958	+1 (+0.10%)
Mathlib.NumberTheory.RamificationInertia.Basic	1920	1922	+2 (+0.10%)
Mathlib.RingTheory.Localization.AtPrime.Extension	1921	1923	+2 (+0.10%)
Mathlib.Analysis.Convex.Segment	962	963	+1 (+0.10%)
Mathlib.RingTheory.DedekindDomain.Factorization	1928	1930	+2 (+0.10%)
Mathlib.RingTheory.DedekindDomain.AdicValuation	1935	1937	+2 (+0.10%)
Mathlib.LinearAlgebra.Finsupp.VectorSpace	983	984	+1 (+0.10%)
Mathlib.Analysis.Convex.Extreme	984	985	+1 (+0.10%)
Mathlib.LinearAlgebra.StdBasis	986	987	+1 (+0.10%)
Mathlib.Algebra.Polynomial.Sequence	993	994	+1 (+0.10%)
Mathlib.RingTheory.Trace.Quotient	1988	1990	+2 (+0.10%)
Mathlib.RingTheory.FractionalIdeal.Norm	1990	1992	+2 (+0.10%)
Mathlib.RingTheory.Flat.TorsionFree	2017	2019	+2 (+0.10%)
Mathlib.RingTheory.Ideal.Operations	1036	1037	+1 (+0.10%)
Mathlib.RingTheory.Ideal.Maps	1039	1040	+1 (+0.10%)
Mathlib.NumberTheory.RamificationInertia.Galois	2112	2114	+2 (+0.09%)
Mathlib.RingTheory.Ideal.Norm.RelNorm	2121	2123	+2 (+0.09%)
Mathlib.RingTheory.Polynomial.Tower	1070	1071	+1 (+0.09%)
Mathlib.MeasureTheory.Group.Integral	2151	2153	+2 (+0.09%)
Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90	2175	2177	+2 (+0.09%)
Mathlib.NumberTheory.Cyclotomic.Basic	2193	2195	+2 (+0.09%)
Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral	2194	2196	+2 (+0.09%)
Mathlib.RingTheory.Ideal.Over	1115	1116	+1 (+0.09%)
Mathlib.NumberTheory.RamificationInertia.Unramified	2233	2235	+2 (+0.09%)
Mathlib.Algebra.Polynomial.Roots	1117	1118	+1 (+0.09%)
Mathlib.RingTheory.Localization.Ideal	1122	1123	+1 (+0.09%)
Mathlib.Topology.Algebra.Module.Basic	1125	1126	+1 (+0.09%)
Mathlib.RingTheory.DedekindDomain.Different	2265	2267	+2 (+0.09%)
Mathlib.Topology.Algebra.Module.LinearMap	1137	1138	+1 (+0.09%)
Mathlib.RingTheory.Algebraic.Cardinality	1144	1145	+1 (+0.09%)
Mathlib.RingTheory.DedekindDomain.LinearDisjoint	2289	2291	+2 (+0.09%)
Mathlib.RingTheory.SimpleModule.Basic	1145	1146	+1 (+0.09%)
Mathlib.Analysis.Convex.Strict	1146	1147	+1 (+0.09%)
Mathlib.RingTheory.Localization.AtPrime.Basic	1150	1151	+1 (+0.09%)
Mathlib.FieldTheory.Tower	1179	1180	+1 (+0.08%)
Mathlib.RingTheory.Polynomial.Content	1191	1192	+1 (+0.08%)
Mathlib.LinearAlgebra.Dimension.Constructions	1244	1245	+1 (+0.08%)
Mathlib.LinearAlgebra.Dimension.Finite	1245	1246	+1 (+0.08%)
Mathlib.LinearAlgebra.Dimension.RankNullity	1246	1247	+1 (+0.08%)
Mathlib.RingTheory.Polynomial.Eisenstein.Basic	1247	1248	+1 (+0.08%)
Mathlib.LinearAlgebra.FreeModule.PID	1259	1260	+1 (+0.08%)
Mathlib.Algebra.Lie.Submodule	1279	1280	+1 (+0.08%)
Mathlib.LinearAlgebra.Eigenspace.Basic	1285	1286	+1 (+0.08%)
Mathlib.LinearAlgebra.Eigenspace.Matrix	1286	1287	+1 (+0.08%)
Mathlib.RingTheory.Filtration	1294	1295	+1 (+0.08%)
Mathlib.RingTheory.Algebraic.Basic	1295	1296	+1 (+0.08%)
Mathlib.Algebra.AlgebraicCard	1298	1299	+1 (+0.08%)
Mathlib.Algebra.Module.Torsion.Basic	1298	1299	+1 (+0.08%)
Mathlib.RingTheory.AdicCompletion.Noetherian	1298	1299	+1 (+0.08%)
Mathlib.Algebra.Module.Lattice	1312	1313	+1 (+0.08%)
Mathlib.RingTheory.FractionalIdeal.Basic	1314	1315	+1 (+0.08%)
Mathlib.Analysis.Convex.Between	1338	1339	+1 (+0.07%)
Mathlib.Analysis.Normed.Module.Ball.Action	1351	1352	+1 (+0.07%)
Mathlib.LinearAlgebra.Reflection	1357	1358	+1 (+0.07%)
Mathlib.RingTheory.FractionalIdeal.Operations	1360	1361	+1 (+0.07%)
Mathlib.LinearAlgebra.BilinearForm.Properties	1376	1377	+1 (+0.07%)
Mathlib.LinearAlgebra.BilinearForm.DualLattice	1377	1378	+1 (+0.07%)
Mathlib.Algebra.Lie.Sl2	1387	1388	+1 (+0.07%)
Mathlib.RingTheory.Coalgebra.GroupLike	1387	1388	+1 (+0.07%)
Mathlib.RingTheory.LocalRing.Quotient	1430	1431	+1 (+0.07%)
Mathlib.Analysis.SpecificLimits.Normed	1493	1494	+1 (+0.07%)
Mathlib.LinearAlgebra.RootSystem.Defs	1515	1516	+1 (+0.07%)
Mathlib.NumberTheory.NumberField.Discriminant.Different	3098	3100	+2 (+0.06%)
Mathlib.RingTheory.Support	1587	1588	+1 (+0.06%)

Import changes for all files

Files	Import difference
There are 3515 files with changed transitive imports taking up over 159597 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
+ Ideal.iInf_pow_smul_eq_bot_of_isTorsionFree
+ IsHausdorff.of_isTorsionFree
+ Module.free_iff_isTorsionFree
+ _root_.Module.IsTorsionFree.of_isLocalization
+ instIsTorsionFreeInteger
+ instance (f : K[X]) : Module.IsTorsionFree K f.SplittingField
+ instance (priority := 100) IsReflexive.to_isTorsionFree : IsTorsionFree R M
+ instance (priority := 100) IsTorsionFree.to_faithfulSMul [Nontrivial A] [IsTorsionFree R A] :
+ instance (priority := 100) instIsTorsionFree : IsTorsionFree R M
+ instance : IsTorsionFree (CyclotomicRing n A K) (CyclotomicField n K)
+ instance : IsTorsionFree (𝓞 K) (𝓞 L)
+ instance : IsTorsionFree (𝓞 K) K
+ instance : IsTorsionFree (𝓞 K) L := .trans_faithfulSMul (𝓞 K) (𝓞 L) L
+ instance : IsTorsionFree R Sₚ := by
+ instance : IsTorsionFree S Sₚ := by
+ instance : Module.IsTorsionFree R (v.adicCompletionIntegers K) := .of_smul_eq_zero <| by simp
+ instance : Module.IsTorsionFree S T := Subalgebra.instIsTorsionFree (integralClosure S E)
+ instance [IsDedekindDomain R] [IsTorsionFree R M] : Flat R M := by
+ instance [IsDomain A] [IsFractionRing A K] : IsTorsionFree A (CyclotomicRing n A K)
+ instance [IsDomain A] [IsFractionRing A K] : Module.IsTorsionFree A (CyclotomicField n K) := by
+ instance [IsDomain R] [IsDomain S] [IsTorsionFree R S] [Module.Finite R S] :
+ instance [IsTorsionFree S T] : IsTorsionFree Sₚ Tₚ
+ instance [IsTorsionFree S T] [Algebra.IsSeparable L F] :
+ instance [Module.IsTorsionFree R M] : Module.IsTorsionFree R N
+ instance [Module.IsTorsionFree S M₂] : Module.IsTorsionFree S (MultilinearMap R M₁ M₂)
+ instance {R S : Type*} [CommRing R] [IsDomain R] {P : Ideal R} [CommRing S] [Algebra R S]
+ int_of_charZero
+ smul_left_inj
+ smul_left_injective
+ smul_right_inj
+ smul_right_injective
++ instIsTorsionFree
++-- aeval_algebraMap_eq_zero_iff
+-+- linearIndependent_single_of_ne_zero
+--+ mk'
- Ideal.iInf_pow_smul_eq_bot_of_noZeroSMulDivisors
- IsHausdorff.of_noZeroSMulDivisors
- Module.free_iff_noZeroSMulDivisors
- NoZeroSMulDivisors.int_of_charZero
- _root_.NoZeroSMulDivisors_of_isLocalization
- instNoZeroSMulDivisors
- instNoZeroSMulDivisorsInteger
- instance (f : K[X]) : NoZeroSMulDivisors K f.SplittingField
- instance (priority := 100) [IsDomain R] : NoZeroSMulDivisors R M := by
- instance (priority := 100) noZeroSMulDivisors [NoZeroDivisors R] : NoZeroSMulDivisors R M
- 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 : NoZeroSMulDivisors S T := Subalgebra.noZeroSMulDivisors_bot (integralClosure S E)
- instance [IsDedekindDomain R] [NoZeroSMulDivisors R M] : Flat R M := by
- instance [IsDomain R] [IsDomain S] [NoZeroSMulDivisors R S] [Module.Finite R S] :
- instance [IsFractionRing A K] :
- instance [IsFractionRing A K] : NoZeroSMulDivisors A (CyclotomicField n K) := by
- instance [NoZeroSMulDivisors R M] : NoZeroSMulDivisors R N
- instance [NoZeroSMulDivisors S T] : NoZeroSMulDivisors Sₚ Tₚ
- instance [NoZeroSMulDivisors S T] [Algebra.IsSeparable L F] :
- instance {R S : Type*} [CommRing R] [NoZeroDivisors R] {P : Ideal R} [CommRing S] [Algebra R S]
- noZeroSMulDivisors

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.

---

No changes to technical debt.

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).

[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.

[mathlib4-merge-conflict-bot]

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

[jcommelin]

Thank you so so much for this heroic effort!

The review was surprisingly pleasant!

[jcommelin]

Thanks 🎉

If CI passes, please merge this yourself, by adding a comment bors r+.

bors d+

[mathlib-bors]

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[YaelDillies]

🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Post-Build Step
• Build
• Lint style

[alreadydone]

This justifies replacing [Ring R] [Nontrivial M] [NoZeroSMulDivisors R M] with [Ring R] [IsDomain R] [Nontrivial M] [IsTorsionFree R M].

I wonder why you use IsDomain R instead of NoZeroDivisors R? The former is equivalent to the latter + Nontrivial R assuming Ring R, but Nontrivial M implies Nontrivial R, so assuming the latter should always be enough. If you use the NoZeroDivisors, users of the lemmas would never need to repeat this argument to supply IsDomain from NoZeroDivisors.

[YaelDillies]

This is the same reason why we write [Ring R] [AddCommGroup M] [Module R M] instead of [Ring R] [AddCommMonoid M] [Module R M]: in the presence of multiple equivalent spellings, we use the strongest one according to TC search. I do not exclude having messed something up, though. Feel free to point out if I really have ungeneralised something!