nonunits_add

Mathlib.RingTheory.LocalRing.Basic

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

← MathLib Explorer

English

In a local ring, the sum of two nonunits is a nonunit.

Русский

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

LaTeX

$$$$\forall a,b\in R,\; a,b\in\text{nonunits }R \Rightarrow a+b \in \text{nonunits }R.$$$$

Lean4

theorem nonunits_add {a b : R} (ha : a ∈ nonunits R) (hb : b ∈ nonunits R) : a + b ∈ nonunits R := fun H =>
  not_or_intro ha hb (isUnit_or_isUnit_of_isUnit_add H)

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

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

Разделы

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

Аффилиация

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