natCast_mem_one

Mathlib.Algebra.Ring.Submonoid.Pointwise

URI: https://scilib.ai/kg/mathlib#AddSubmonoid.natCast_mem_one

English

For every natural number n, its image n in R lies in the submonoid generated by 1.

Русский

Для каждого натурального числа n образ n в R принадлежит подмоноиду, порождаемому единицей.

LaTeX

$$$\forall n \in \mathbb{N}, (n : R) \in (1 : AddSubmonoid R)$$$

Lean4

theorem natCast_mem_one (n : ℕ) : (n : R) ∈ (1 : AddSubmonoid R) :=
  ⟨_, rfl⟩

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

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

Разделы

Аффилиация

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