one_mem_toNonUnitalSubring

Mathlib.Algebra.Ring.Subring.Defs

URI: https://scilib.ai/kg/mathlib#Subring.one_mem_toNonUnitalSubring

English

The multiplicative identity 1 belongs to the nonunital subring underlying any Subring S of a ring R.

Русский

Единица принадлежит подкольцу, лежащему внутри подкольца S кольца R.

LaTeX

$$$1 \in S$$$

Lean4

theorem one_mem_toNonUnitalSubring (S : Subring R) : 1 ∈ S.toNonUnitalSubring :=
  S.one_mem

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

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

Разделы

Аффилиация

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