addSubgroupClosure_one — Mathlib

English

In the additive group of integers, the closure of {1} is the entire group: AddSubgroup.closure({1}) = ⊤.

Русский

В аддитивной группе целых чисел замыкание множества {1} равно всей группе: closure({1}) = ⊤.

LaTeX

$$$\operatorname{AddSubgroup.closure}(\{1\}) = \top$$$

Lean4

@[simp]
theorem addSubgroupClosure_one : AddSubgroup.closure ({ 1 } : Set ℤ) = ⊤ :=
  by
  ext
  simp [AddSubgroup.mem_closure_singleton]

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