NoZeroSMulDivisors

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

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 two_nsmul_eq_zero (R : Type u_3) (M : Type u_4) [Semiring R] [CharZero R] [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors R M] {v : M} : 2 • v = 0 ↔ v = 0

theorem CharZero.of_module (R : Type u_1) [Semiring R] (M : Type u_3) [AddCommMonoidWithOne M] [CharZero M] [Module R M] : CharZero R

If M is an R-module with one and M has characteristic zero, then R has characteristic zero as well. Usually M is an R-algebra.

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 self_eq_neg (R : Type u_3) (M : Type u_4) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {v : M} : v = -v ↔ v = 0

theorem neg_eq_self (R : Type u_3) (M : Type u_4) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {v : M} : -v = v ↔ v = 0

theorem self_ne_neg (R : Type u_3) (M : Type u_4) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {v : M} : v ≠ -v ↔ v ≠ 0

theorem neg_ne_self (R : Type u_3) (M : Type u_4) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {v : M} : -v ≠ v ↔ v ≠ 0

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

instance instNoZeroSMulDivisorsNatOfInt {M : Type u_2} [AddCommGroup M] [NoZeroSMulDivisors ℤ M] : NoZeroSMulDivisors ℕ M

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] [NoZeroSMulDivisors ℤ M] : CharZero R

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

instance instNoZeroSMulDivisorsNatOfInt_1 (M : Type u_2) [AddCommGroup M] [NoZeroSMulDivisors ℤ M] : NoZeroSMulDivisors ℕ M

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