intCast_mem — Mathlib

English

Every subring S of R contains the image of all integers under the canonical embedding; i.e., for all n ∈ ℤ, (n : R) ∈ S.

Русский

Каждое подкольцо S ⊆ R содержит изображение всех целых чисел через каноническое отображение; то есть для каждого n ∈ ℤ, (n : R) ∈ S.

LaTeX

$$$\forall n\in \mathbb{Z},\ (n:\!R)\in S$$$

Lean4

@[simp, aesop safe (rule_sets := [SetLike])]
theorem intCast_mem (n : ℤ) : (n : R) ∈ s := by simp only [← zsmul_one, zsmul_mem, one_mem]

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