natCast_mem — Mathlib

English

Let S be a subalgebra of A over R. Then every natural number, viewed inside A via the canonical embedding n ↦ n in A, lies in S.

Русский

Пусть S—подалгебра над R внутри A. Тогда каждое естественное число, воспринятое как элемент A через естественное включение n ↦ n, принадлежит S.

LaTeX

$$$$ \\forall n:\\\\mathbb{N},\\ (n:A)\\in S $$$$

Lean4

protected theorem natCast_mem (n : ℕ) : (n : A) ∈ S :=
  natCast_mem S n

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