comap_nonZeroDivisors_le_of_injective

English

A symmetric formulation: comap preserves nonzero divisors under an injective map in the opposite direction, i.e., kernel-free transfer of divisors.

Русский

Симметричная формулировка: обратная проекция сохраняет ненулевые делители при инъективном отображении.

LaTeX

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

Lean4

theorem comap_nonZeroDivisors_le_of_injective [MonoidWithZeroHomClass F M₀ M₀'] {f : F} (hf : Injective f) :
    M₀'⁰.comap f ≤ M₀⁰ := fun _ ha ↦ mem_nonZeroDivisors_of_injective hf (Submonoid.mem_comap.mp ha)

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