English
If R is a semiring with CharZero and M is an AddCommMonoid with a Module structure, and NoZeroSMulDivisors R M holds, then NoZeroSMulDivisors Nat M holds. In particular, for natural scalars, a nonzero scalar cannot annihilate a nonzero vector.
Русский
Если R — полупазывающий полукольцо с характеристикой ноль и M — аддитивная коммргруппа с модульной структурой, и выполняется NoZeroSMulDivisors R M, то для ℕ-масштаба верно NoZeroSMulDivisors ℕ M: ненулевой скаляр не аннигилирует ненулевой элемент.
LaTeX
$$$\forall c \in \mathbb{N}, \forall x \in M,\ (c \cdot x = 0) \Rightarrow (c = 0 \lor x = 0)$$$
Lean4
theorem noZeroSMulDivisors (R) (M) [Semiring R] [CharZero R] [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors R M] :
NoZeroSMulDivisors ℕ M where
eq_zero_or_eq_zero_of_smul_eq_zero {c x} := by rw [← Nat.cast_smul_eq_nsmul R, smul_eq_zero]; simp
