NoZeroSMulDivisors

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

class NoZeroSMulDivisors (R : Type u_4) (M : Type u_5) [Zero R] [Zero M] [SMul R M] : Prop

NoZeroSMulDivisors R M states that a scalar multiple is 0 only if either argument is 0. This is a version of saying that M is torsion free, without assuming R is zero-divisor free.

The main application of NoZeroSMulDivisors R M, when M is a module, is the result smul_eq_zero: a scalar multiple is 0 iff either argument is 0.

It is a generalization of the NoZeroDivisors class to heterogeneous multiplication.

• eq_zero_or_eq_zero_of_smul_eq_zero {c : R} {x : M} : c • x = 0 → c = 0 ∨ x = 0

  If scalar multiplication yields zero, either the scalar or the vector was zero.

theorem noZeroSMulDivisors_iff (R : Type u_4) (M : Type u_5) [Zero R] [Zero M] [SMul R M] : NoZeroSMulDivisors R M ↔ ∀ {c : R} {x : M}, c • x = 0 → c = 0 ∨ x = 0

theorem Function.Injective.noZeroSMulDivisors {R : Type u_4} {M : Type u_5} {N : Type u_6} [Zero R] [Zero M] [Zero N] [SMul R M] [SMul R N] [NoZeroSMulDivisors R N] (f : M → N) (hf : Injective f) (h0 : f 0 = 0) (hs : ∀ (c : R) (x : M), f (c • x) = c • f x) : NoZeroSMulDivisors R M

Pullback a NoZeroSMulDivisors instance along an injective function.

@[instance 100]

instance NoZeroDivisors.toNoZeroSMulDivisors {R : Type u_1} [Zero R] [Mul R] [NoZeroDivisors R] : NoZeroSMulDivisors R R

theorem smul_ne_zero {R : Type u_1} {M : Type u_2} [Zero R] [Zero M] [SMul R M] [NoZeroSMulDivisors R M] {c : R} {x : M} (hc : c ≠ 0) (hx : x ≠ 0) : c • x ≠ 0

@[simp]

theorem smul_eq_zero {R : Type u_1} {M : Type u_2} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M} : c • x = 0 ↔ c = 0 ∨ x = 0

theorem smul_ne_zero_iff {R : Type u_1} {M : Type u_2} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M} : c • x ≠ 0 ↔ c ≠ 0 ∧ x ≠ 0

theorem smul_eq_zero_iff_left {R : Type u_1} {M : Type u_2} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M} (hx : x ≠ 0) : c • x = 0 ↔ c = 0

theorem smul_eq_zero_iff_right {R : Type u_1} {M : Type u_2} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M} (hc : c ≠ 0) : c • x = 0 ↔ x = 0

theorem smul_ne_zero_iff_left {R : Type u_1} {M : Type u_2} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M} (hx : x ≠ 0) : c • x ≠ 0 ↔ c ≠ 0

theorem smul_ne_zero_iff_right {R : Type u_1} {M : Type u_2} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M} (hc : c ≠ 0) : c • x ≠ 0 ↔ x ≠ 0

instance IsAddTorsionFree.to_noZeroSMulDivisors_nat {M : Type u_2} [AddMonoid M] [IsAddTorsionFree M] : NoZeroSMulDivisors ℕ M

instance IsAddTorsionFree.to_noZeroSMulDivisors_int {G : Type u_3} [AddGroup G] [IsAddTorsionFree G] : NoZeroSMulDivisors ℤ G

@[simp]

theorem noZeroSMulDivisors_nat_iff_isAddTorsionFree {G : Type u_3} [AddCommGroup G] : NoZeroSMulDivisors ℕ G ↔ IsAddTorsionFree G

@[simp]

theorem noZeroSMulDivisors_int_iff_isAddTorsionFree {G : Type u_3} [AddCommGroup G] : NoZeroSMulDivisors ℤ G ↔ IsAddTorsionFree G

theorem IsAddTorsionFree.of_noZeroSMulDivisors_nat {G : Type u_3} [AddCommGroup G] : NoZeroSMulDivisors ℕ G → IsAddTorsionFree G

Alias of the forward direction of noZeroSMulDivisors_nat_iff_isAddTorsionFree.

theorem IsAddTorsionFree.of_noZeroSMulDivisors_int {G : Type u_3} [AddCommGroup G] : NoZeroSMulDivisors ℤ G → IsAddTorsionFree G

Alias of the forward direction of noZeroSMulDivisors_int_iff_isAddTorsionFree.