Integer Complement

We define the complement of the integers in the complex plane and give some basic lemmas about it. We also show that the upper half plane embeds into the integer complement.

def Complex.integerComplement : Set ℂ

The complement of the integers in ℂ

theorem Complex.integerComplement_eq : integerComplement = {z : ℂ | ¬∃ (n : ℤ), ↑n = z}

theorem Complex.mem_integerComplement_iff {x : ℂ} : x ∈ integerComplement ↔ ¬∃ (n : ℤ), ↑n = x

@[deprecated Complex.mem_integerComplement_iff (since := "2026-01-29")]

theorem Complex.integerComplement.mem_iff {x : ℂ} : x ∈ integerComplement ↔ ¬∃ (n : ℤ), ↑n = x

Alias of Complex.mem_integerComplement_iff.

@[simp]

theorem UpperHalfPlane.coe_mem_integerComplement (z : UpperHalfPlane) : ↑z ∈ Complex.integerComplement

@[simp]

theorem Complex.add_intCast_mem_integerComplement {x : ℂ} (a : ℤ) : x + ↑a ∈ integerComplement ↔ x ∈ integerComplement

@[deprecated Complex.add_intCast_mem_integerComplement (since := "2026-01-29")]

theorem Complex.integerComplement.add_coe_int_mem {x : ℂ} (a : ℤ) : x + ↑a ∈ integerComplement ↔ x ∈ integerComplement

Alias of Complex.add_intCast_mem_integerComplement.

theorem Complex.integerComplement.ne_zero {x : ℂ} (hx : x ∈ integerComplement) : x ≠ 0

theorem Complex.integerComplement_add_ne_zero {x : ℂ} (hx : x ∈ integerComplement) (a : ℤ) : x + ↑a ≠ 0

theorem Complex.integerComplement.ne_one {x : ℂ} (hx : x ∈ integerComplement) : x ≠ 1

theorem Complex.integerComplement_pow_two_ne_pow_two {x : ℂ} (hx : x ∈ integerComplement) (n : ℤ) : x ^ 2 ≠ ↑n ^ 2

theorem Complex.upperHalfPlane_inter_integerComplement : {z : ℂ | 0 < z.im} ∩ integerComplement = {z : ℂ | 0 < z.im}

theorem UpperHalfPlane.int_div_mem_integerComplement (z : UpperHalfPlane) {n : ℤ} (hn : n ≠ 0) : ↑n / ↑z ∈ Complex.integerComplement