Commit 2024-11-15 10:19 672417d0

View on Github →

feat(Analysis): integer complement in ℂ (#16542) Develop some basic API for the complement of the integers in the complex numbers.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Complex/Basic.lean

added theorem Complex.closedEmbedding_intCast

added theorem Complex.isClosed_range_intCast

added theorem Complex.isOpen_compl_range_intCast

added theorem Complex.isometry_intCast

Created Mathlib/Analysis/Complex/IntegerCompl.lean

added theorem Complex.UpperHalfPlane.coe_mem_integerComplement

added theorem Complex.integerComplement.add_coe_int_mem

added theorem Complex.integerComplement.mem_iff

added theorem Complex.integerComplement.ne_one

added theorem Complex.integerComplement.ne_zero

added def Complex.integerComplement

added theorem Complex.integerComplement_add_ne_zero

added theorem Complex.integerComplement_eq

Modified Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

added theorem UpperHalfPlane.ne_int

added theorem UpperHalfPlane.ne_nat