Commit 2026-01-13 19:40 290f644e

View on Github →

chore(Algebra): replace NoZeroSMulDivisors with Module.IsTorsionFree wlog (#30563) 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.

Estimated changes

modified theorem finsum_smul
modified theorem infinite_range_add_smul_iff
added theorem smul_left_inj
added theorem smul_left_injective
added theorem smul_right_inj
added theorem smul_right_injective
deleted theorem Nat.noZeroSMulDivisors
deleted theorem smul_left_injective
deleted theorem smul_right_inj
deleted theorem smul_right_injective
modified theorem Polynomial.aroots_C_mul
modified theorem Polynomial.aroots_monomial
modified theorem Polynomial.aroots_mul
modified theorem Polynomial.mem_aroots
modified theorem Polynomial.mem_rootSet
modified theorem Polynomial.rootSet_mapsTo
modified theorem Sbtw.not_rotate
modified theorem Sbtw.not_swap_left
modified theorem Sbtw.not_swap_right
modified theorem Sbtw.trans_left
modified theorem Sbtw.trans_right
modified theorem Sbtw.trans_wbtw_left_ne
modified theorem Sbtw.trans_wbtw_right_ne
modified theorem Wbtw.rotate_iff
modified theorem Wbtw.swap_left_iff
modified theorem Wbtw.swap_right_iff
modified theorem Wbtw.trans_left_ne
modified theorem Wbtw.trans_right_ne
modified theorem Wbtw.trans_sbtw_left
modified theorem Wbtw.trans_sbtw_right
modified theorem sbtw_lineMap_iff
modified theorem sbtw_mul_sub_add_iff
modified theorem wbtw_lineMap_iff
modified theorem wbtw_mul_sub_add_iff
modified theorem wbtw_rotate_iff
modified theorem wbtw_swap_left_iff
modified theorem wbtw_swap_right_iff
modified theorem left_mem_openSegment_iff
modified theorem right_mem_openSegment_iff
modified theorem Finsupp.nonTorsionWeight_of
modified theorem Module.Finite.left
modified theorem AffineMap.lineMap_injective
modified theorem LinearMap.ker_lsmul
modified theorem LinearMap.lsmul_injective
modified theorem iSupIndep.linearIndependent
modified theorem Module.finrank_pos
modified theorem Module.finrank_pos_iff
modified theorem Module.finrank_zero_iff
modified theorem Submodule.finrank_eq_zero
modified theorem Submodule.rank_eq_zero
modified theorem Module.Ray.ne_neg_self
modified theorem eq_zero_of_sameRay_self_neg
modified def RootPairing.mk'
modified def RootPairing.Equiv.mk'
modified theorem Ideal.inertiaDegIn_ne_zero
modified theorem IsIntegralClosure.rank
modified theorem Ideal.primesOver_bot
modified theorem Ideal.map_ne_bot_of_ne_bot
modified theorem Module.punctured_nhds_neBot