`NoZeroSMulDivisors` #

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

Usage notes #

Note that NoZeroSMulDivisors is deprecated in favor of Module.IsTorsionFree, which is the mathematically correct generalisation to semimodules.

source

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.

Instances

source

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

source

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.

source

@[instance 100]