isUnitSubmonoid_eq

Mathlib.RingTheory.Artinian.Module

URI: https://scilib.ai/kg/mathlib#IsArtinianRing.isUnitSubmonoid_eq

English

In an Artinian ring, the submonoid of units equals the set of non-zero divisors.

Русский

В артиновом кольце подмножество единиц совпадает с множеством не нулевых делителей.

LaTeX

$$$\mathrm{IsUnit.submonoid}(R) = R^{0}$$$

Lean4

theorem isUnitSubmonoid_eq [IsArtinianRing R] : IsUnit.submonoid R = R⁰ := by ext;
  simp [IsUnit.mem_submonoid_iff, isUnit_iff_mem_nonZeroDivisors]

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

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

Разделы

Аффилиация

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