add_coe_int_mem — Mathlib

English

For any complex x and integer a, the membership of x + a in ℂ_ℤ is equivalent to membership of x in ℂ_ℤ.

Русский

Для любого комплексного x и целого a, членство x + a в ℂ_ℤ эквивалентно членству x в ℂ_ℤ.

LaTeX

$$$\\forall x \\in \\mathbb{C}, \\forall a \\in \\mathbb{Z}, \\; x + a \\in \\mathbb{C}_{\\mathbb{Z}} \\iff x \\in \\mathbb{C}_{\\mathbb{Z}}.$$$

Lean4

theorem add_coe_int_mem {x : ℂ} (a : ℤ) : x + (a : ℂ) ∈ ℂ_ℤ ↔ x ∈ ℂ_ℤ :=
  by
  simp only [mem_iff, not_iff_not]
  exact ⟨(Exists.elim · fun n hn ↦ ⟨n - a, by simp [hn]⟩), (Exists.elim · fun n hn ↦ ⟨n + a, by simp [hn]⟩)⟩

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