isRegular_iff_mem_nonZeroDivisors

Mathlib.Algebra.Ring.NonZeroDivisors

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

English

In a ring, IsRegular r iff r ∈ R⁰ (the set of non-zero divisors).

Русский

В кольце IsRegular r эквивалентно тому, что r ∈ R⁰ (множество неснулей делителей).

LaTeX

$$$$\\operatorname{IsRegular}(r) \\iff r \\in R^{0}$$$$

Lean4

theorem isRegular_iff_mem_nonZeroDivisors : IsRegular r ↔ r ∈ R⁰ :=
  isRegular_iff_eq_zero_of_mul

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

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

Разделы

Аффилиация

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