HepLean Documentation

Mathlib.Algebra.NoZeroSMulDivisors.Defs

NoZeroSMulDivisors #

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

NoZeroSMulDivisors #

source
theorem noZeroSMulDivisors_iff (R : Type u_3) (M : Type u_4) [Zero R] [Zero M] [SMul R M] :
NoZeroSMulDivisors R M ↔ ∀ {c : R} {x : M}, c • x = 0 → c = 0 ∨ x = 0
source
class NoZeroSMulDivisors (R : Type u_3) (M : Type u_4) [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.eq_zero_or_eq_zero_of_smul_eq_zero {R : Type u_3} {M : Type u_4} :
    ∀ {inst : Zero R} {inst_1 : Zero M} {inst_2 : SMul R M} [self : NoZeroSMulDivisors R M] {c : R} {x : M}, c • x = 0 → c = 0 ∨ x = 0

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

    source
    theorem Function.Injective.noZeroSMulDivisors {R : Type u_3} {M : Type u_4} {N : Type u_5} [Zero R] [Zero M] [Zero N] [SMul R M] [SMul R N] [NoZeroSMulDivisors R N] (f : M → N) (hf : Function.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]
    instance NoZeroDivisors.toNoZeroSMulDivisors {R : Type u_1} [Zero R] [Mul R] [NoZeroDivisors R] :
    NoZeroSMulDivisors R R
    Equations
    • ⋯ = ⋯
    source
    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
    source
    @[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
    source
    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
    source
    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
    source
    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
    source
    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
    source
    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