NoZeroSMulDivisors

This file defines the NoZeroSMulDivisors class, and includes some tests for the vanishing of elements (especially in modules over division rings).

theorem smul_right_injective {R : Type u_1} (M : Type u_2) [Semiring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {c : R} (hc : c ≠ 0) : Function.Injective fun (x : M) => c • x

theorem smul_right_inj {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {c : R} (hc : c ≠ 0) {x y : M} : c • x = c • y ↔ x = y

theorem IsAddTorsionFree.of_noZeroSMulDivisors (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommGroup M] [Module R M] [CharZero R] [NoZeroSMulDivisors R M] : IsAddTorsionFree M

@[deprecated IsAddTorsionFree.of_noZeroSMulDivisors (since := "2025-10-19")]

theorem Nat.noZeroSMulDivisors (R : Type u_3) (M : Type u_4) [Semiring R] [CharZero R] [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors R M] : NoZeroSMulDivisors ℕ M

theorem smul_left_injective (R : Type u_1) {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {x : M} (hx : x ≠ 0) : Function.Injective fun (c : R) => c • x

@[deprecated IsAddTorsionFree.of_noZeroSMulDivisors (since := "2025-10-19")]

theorem NoZeroSMulDivisors.int_of_charZero (R : Type u_3) (M : Type u_4) [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [CharZero R] : NoZeroSMulDivisors ℤ M

theorem CharZero.of_noZeroSMulDivisors (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] [Nontrivial M] [IsAddTorsionFree M] : CharZero R

Only a ring of characteristic zero can have a non-trivial module without additive or scalar torsion.

@[instance 100]

instance GroupWithZero.toNoZeroSMulDivisors {R : Type u_1} {M : Type u_2} [GroupWithZero R] [AddMonoid M] [DistribMulAction R M] : NoZeroSMulDivisors R M

This instance applies to DivisionSemirings, in particular NNReal and NNRat.