le_nonZeroDivisors_iff_isRegular — Mathlib

English

For a submonoid S of R, S ≤ R⁰ iff every s in S is IsRegular.

Русский

Для подмоноида S в кольце R, S ≤ R⁰ тогда и только тогда, когда каждый элемент S является IsRegular.

LaTeX

$$$$S \\leq R^{0} \\iff \\forall s : S, \\operatorname{IsRegular}(s)$$$$

Lean4

theorem le_nonZeroDivisors_iff_isRegular {S : Submonoid R} : S ≤ R⁰ ↔ ∀ s : S, IsRegular (s : R) := by
  simp_rw [nonZeroDivisors, le_inf_iff, le_nonZeroDivisorsLeft_iff_isLeftRegular,
    le_nonZeroDivisorsRight_iff_isRightRegular, isRegular_iff, forall_and]

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