ofNat_mem_center — Mathlib

English

Let M be a (not necessarily associative) semiring. For every natural number n with n ≥ 2, the natural embedding of n into M is central; i.e. (n : M) lies in the center of M, commuting with every element of M.

Русский

Пусть M — неассоциативное полукольцо. Для любого натурального числа n, большего либо равного 2, образ числа n в M лежит в центре M; то есть (n : M) коммутирует со всяким элементом M.

LaTeX

$$$(n : M) \\in \\operatorname{Center}(M) \\quad\\text{for all } n \\in \\mathbb{N},\\ n \\ge 2.$$$

Lean4

@[simp]
theorem ofNat_mem_center [NonAssocSemiring M] (n : ℕ) [n.AtLeastTwo] : ofNat(n) ∈ Set.center M :=
  natCast_mem_center M n

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