isLeftRegular_iff_mem_nonZeroDivisorsLeft

Mathlib.Algebra.Ring.NonZeroDivisors

URI: https://scilib.ai/kg/mathlib#isLeftRegular_iff_mem_nonZeroDivisorsLeft

English

In a ring R, IsLeftRegular r iff r belongs to nonZeroDivisorsLeft R.

Русский

В кольце R IsLeftRegular r тогда и только тогда, когда r принадлежит nonZeroDivisorsLeft R.

LaTeX

$$$$\\operatorname{IsLeftRegular}(r) \\iff r \\in \\text{nonZeroDivisorsLeft } R$$$$

Lean4

theorem isLeftRegular_iff_mem_nonZeroDivisorsLeft : IsLeftRegular r ↔ r ∈ nonZeroDivisorsLeft R :=
  isLeftRegular_iff_right_eq_zero_of_mul

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru