nonZeroDivisors_le_comap_nonZeroDivisors_of_injective

English

If f is injective, then every nonzero-divisor of M0 is carried back to a nonzero-divisor of M0'. Concretely, M0⁰ ≤ (M0'⁰).comap f.

Русский

Если f инъективно отображает M0 в M0', то любой ненулевой делитель в M0 отображается обратно в ненулевой делитель в M0'.

LaTeX

$$nonZeroDivisors_le_comap_nonZeroDivisors_of_injective [NoZeroDivisors M0'] [MonoidWithZeroHomClass F M0 M0'] (f : F) (hf : Injective f) : M0⁰ ≤ M0'⁰.comap f$$

Lean4

theorem nonZeroDivisors_le_comap_nonZeroDivisors_of_injective [NoZeroDivisors M₀'] [MonoidWithZeroHomClass F M₀ M₀']
    (f : F) (hf : Injective f) : M₀⁰ ≤ M₀'⁰.comap f :=
  Submonoid.le_comap_of_map_le _ (map_le_nonZeroDivisors_of_injective _ hf le_rfl)

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