isUnit_of_mem_nonZeroDivisors

Mathlib.Algebra.GroupWithZero.NonZeroDivisors

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

English

In a Group with zero, every element that is a nonzero-divisor is a unit.

Русский

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

LaTeX

$$isUnit_of_mem_nonZeroDivisors (hx : x ∈ nonZeroDivisors G0) : IsUnit x$$

Lean4

theorem isUnit_of_mem_nonZeroDivisors (hx : x ∈ nonZeroDivisors G₀) : IsUnit x :=
  (nonZeroDivisorsEquivUnits ⟨x, hx⟩).isUnit

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

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

Разделы

Аффилиация

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