map_nonZeroDivisors_le — Mathlib

English

In a localization setting, the image of non-zero divisors from R maps into non-zero divisors of S.

Русский

В локализационной ситуации образ безразделителей нуля из R переходит в безразделители нуля в S.

LaTeX

$$$$ (\\operatorname{nonZeroDivisors} R).\\mathrm{map}(\\text{algebraMap } R S) \\le \\operatorname{nonZeroDivisors} S $$$$

Lean4

theorem map_nonZeroDivisors_le [IsLocalization M S] : (nonZeroDivisors R).map (algebraMap R S) ≤ nonZeroDivisors S :=
  (toLocalizationMap M S).map_nonZeroDivisors_le

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