le_nonZeroDivisorsLeft_iff_isLeftRegular

English

For a submonoid S of R, S ≤ nonZeroDivisorsLeft R iff every s in S is IsLeftRegular.

Русский

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

LaTeX

$$$$S \\leq \\text{nonZeroDivisorsLeft } R \\iff \\forall s \\in S,\; \\operatorname{IsLeftRegular}(s)$$$$

Lean4

theorem le_nonZeroDivisorsLeft_iff_isLeftRegular {S : Submonoid R} :
    S ≤ nonZeroDivisorsLeft R ↔ ∀ s : S, IsLeftRegular (s : R) := by
  simp_rw [SetLike.le_def, isLeftRegular_iff_mem_nonZeroDivisorsLeft, Subtype.forall]

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