le_nonZeroDivisorsRight_iff_isRightRegular

English

For a submonoid S of R, S ≤ nonZeroDivisorsRight R iff every s in S is IsRightRegular.

Русский

Для подмоноида S в кольце R выполняется: S ≤ nonZeroDivisorsRight R тогда и только тогда, когда для каждого s ∈ S выполняется IsRightRegular s.

LaTeX

$$$$S \\leq \\text{nonZeroDivisorsRight } R \\iff \\forall s : S, \\operatorname{IsRightRegular}(s)$$$$

Lean4

theorem le_nonZeroDivisorsRight_iff_isRightRegular {S : Submonoid R} :
    S ≤ nonZeroDivisorsRight R ↔ ∀ s : S, IsRightRegular (s : R) := by
  simp_rw [SetLike.le_def, isRightRegular_iff_mem_nonZeroDivisorsRight, Subtype.forall]

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