map_ne_zero_of_mem_nonZeroDivisors

English

If g is an injective homomorphism of monoids with zero (a NoZeroDivisors-preserving map), and x is a nonzero-divisor in M, then g x ≠ 0 in the target. In particular, injective zero-homomorphisms preserve nonzero divisors.

Русский

Если g — инъективное отображение моноидов с нулём, сохраняющее нулевые делители, и x — ненулевой делитель в M, то g(x) ≠ 0 в целевом множество.

LaTeX

$$[Nontrivial M_0] [ZeroHomClass F M_0 M_0'] (g : F) (hg : Injective (g : M_0 → M_0')) {x : M_0} (h : x ∈ M_0⁰) : g x ≠ 0$$

Lean4

theorem map_ne_zero_of_mem_nonZeroDivisors [Nontrivial M₀] [ZeroHomClass F M₀ M₀'] (g : F)
    (hg : Injective (g : M₀ → M₀')) {x : M₀} (h : x ∈ M₀⁰) : g x ≠ 0 := fun h0 ↦
  one_ne_zero (h.2 1 ((one_mul x).symm ▸ hg (h0.trans (map_zero g).symm)))

Похожие утверждения