English
If f is an injective monoid homomorphism, then the comap of nonzero divisors is contained in the nonzero divisors: nonZeroDivisors M0' comap f ≤ nonZeroDivisors M0.
Русский
Если f — инъективный гомоморфизм, то обратная проекция ненулевых делителей удовлетворяет: M0'⁰ comap f ≤ M0⁰.
LaTeX
$$comap_nonZeroDivisors_le_of_injective [MonoidWithZeroHomClass F M0 M0'] {f : F} (hf : Injective f) : M0'⁰.comap f ≤ M0⁰$$
Lean4
/-- If an element maps to a non-zero-divisor via injective homomorphism,
then it is a non-zero-divisor. -/
theorem mem_nonZeroDivisors_of_injective [MonoidWithZeroHomClass F M₀ M₀'] {f : F} (hf : Injective f)
(hx : f x ∈ M₀'⁰) : x ∈ M₀⁰ :=
⟨fun y hy ↦ hf <| map_zero f ▸ hx.1 (f y) (map_mul f x y ▸ map_zero f ▸ congrArg f hy), fun y hy ↦
hf <| map_zero f ▸ hx.2 (f y) (map_mul f y x ▸ map_zero f ▸ congrArg f hy)⟩
