English
Let M be a type with a zero and a left action by the monoid M0. The action has no zero-smul-divisors if and only if every nonzero element of M0 acts as a nonzero divisor on M; equivalently, NoZeroSMulDivisors M0 M holds exactly when for every x in M0 with x ≠ 0, x is in the nonZeroSMulDivisors M0 M.
Русский
Пусть M — множество с нулём и слева действует моноид M0. Действие не имеет нулевых делителей под действием, если и только если каждый ненулевой элемент M0 является ненулевым делителем под действием на M; эквивалентно: NoZeroSMulDivisors M0 M выполняется тогда и только тогда, когда для любого x ∈ M0, x ≠ 0 следует, что x ∈ nonZeroSMulDivisors M0 M.
LaTeX
$$$NoZeroSMulDivisors\\ M_0\\ M\\iff \\forall x : M_0, x \\ne 0 \\rightarrow x \\in nonZeroSMulDivisors\\ M_0\\ M$$$
Lean4
theorem noZeroSMulDivisors_iff_forall_mem_nonZeroSMulDivisors {M : Type*} [Zero M] [MulAction M₀ M] :
NoZeroSMulDivisors M₀ M ↔ ∀ x : M₀, x ≠ 0 → x ∈ nonZeroSMulDivisors M₀ M :=
noZeroSMulDivisors_iff_right_eq_zero_of_smul
