isUnit_of_mem_nonunits_one_sub_self

Mathlib.RingTheory.LocalRing.Basic

URI: https://scilib.ai/kg/mathlib#IsLocalRing.isUnit_of_mem_nonunits_one_sub_self

← MathLib Explorer

English

In a local ring R, if 1 − a is a nonunit, then a is a unit.

Русский

В локальном кольце R, если 1 − a не единица, то a является единицей.

LaTeX

$$$[\\text{IsLocalRing } R]\\;\\land\\ (1-a) \\notin R^{\\times} \\Rightarrow a \\in R^{\\times}$$$

Lean4

theorem isUnit_of_mem_nonunits_one_sub_self (a : R) (h : 1 - a ∈ nonunits R) : IsUnit a :=
  or_iff_not_imp_right.1 (isUnit_or_isUnit_one_sub_self a) h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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