noZeroDivisors — Mathlib

English

If M has no zero divisors and f is a localization map from M to N, then N also has no zero divisors.

Русский

Если у M нет нулевых делителей, то и у N нет нулевых делителей после локализации по f.

LaTeX

$$$\\text{NoZeroDivisors}(M) \\Rightarrow \\text{NoZeroDivisors}(N)$ for localization $f : S \\to N$.$$

Lean4

theorem noZeroDivisors (f : LocalizationMap S N) [NoZeroDivisors M] : NoZeroDivisors N :=
  by
  refine noZeroDivisors_iff_forall_mem_nonZeroDivisors.mpr fun n hn ↦ ?_
  have ⟨ms, eq⟩ := f.surj n
  have hs : ms.1 ≠ 0 := fun h ↦ hn (by rwa [h, f.map_zero, (f.map_units _).mul_left_eq_zero] at eq)
  exact
    And.left <| mul_mem_nonZeroDivisors.mp (eq ▸ f.map_nonZeroDivisors_le ⟨_, mem_nonZeroDivisors_of_ne_zero hs, rfl⟩)

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