closure_singleton_intCast — Mathlib

English

For any integer n, the closure of {n.cast} is the bottom subring.

Русский

Для любого целого числа n, замыкание множества {n.cast} равно нижнему подкольцу.

LaTeX

$$$\\forall n \\in \\mathbb{Z},\\ \\mathrm{closure}(\\{n\\cast\\}) = \\bot$$$

Lean4

@[simp]
theorem closure_singleton_intCast (n : ℤ) : closure {(n : R)} = ⊥ :=
  bot_unique <| closure_le.2 <| Set.singleton_subset_iff.mpr <| intCast_mem _ _

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