map_nonZeroDivisors_le — Mathlib

English

For a LocalizationMap f, the image of nonZeroDivisors M under f is contained in nonZeroDivisors N.

Русский

Образ множества ненулевых делителей M под f лежит в множестве ненулевых делителей N.

LaTeX

$$(nonZeroDivisors M).map f ≤ nonZeroDivisors N$$

Lean4

theorem map_nonZeroDivisors_le (f : LocalizationMap S N) : (nonZeroDivisors M).map f ≤ nonZeroDivisors N :=
  map_le_iff_le_comap.mpr f.nonZeroDivisors_le_comap

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