English
If g is an injective map of monoids with zero, then x is a nonzero-divisor in M whenever g x is a nonzero-divisor in M'. In particular, nonzero-divisor status is preserved under injective maps.
Русский
Если g — инъективное отображение между мономииями с нулём, то ненулевой делитель сохраняется: если g x — ненулевой делитель в M', то x — ненулевой делитель в M.
LaTeX
$$[Nontrivial M_0] [NoZeroDivisors M_0'] [ZeroHomClass F M_0 M_0'] (g : F) (hg : Injective g) {x : M_0} (h : x ∈ M_0⁰) : g x ∈ M_0'⁰$$
Lean4
theorem map_mem_nonZeroDivisors [Nontrivial M₀] [NoZeroDivisors M₀'] [ZeroHomClass F M₀ M₀'] (g : F) (hg : Injective g)
{x : M₀} (h : x ∈ M₀⁰) : g x ∈ M₀'⁰ :=
⟨fun _ ↦ eq_zero_of_ne_zero_of_mul_left_eq_zero (map_ne_zero_of_mem_nonZeroDivisors g hg h), fun _ ↦
eq_zero_of_ne_zero_of_mul_right_eq_zero (map_ne_zero_of_mem_nonZeroDivisors g hg h)⟩
