isRegular_iff_isUnit_of_finite

Mathlib.Algebra.Ring.NonZeroDivisors

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

English

For a finite ring R, IsRegular r is equivalent to IsUnit r.

Русский

Для конечного кольца R IsRegular r эквивалентно IsUnit r.

LaTeX

$$$$\\operatorname{IsRegular}(r) \\iff \\operatorname{IsUnit}(r)$$$$

Lean4

theorem isRegular_iff_isUnit_of_finite : IsRegular r ↔ IsUnit r
    where
  mp h := h.1.isUnit_of_finite
  mpr h := h.isRegular

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

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

Разделы

Аффилиация

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