@[reducible, inline]

abbrev ComplexTorus (L : ComplexLattice) : Type

The complex torus ℂ / L associated to a ComplexLattice L, viewed as the quotient of the additive group of ℂ by the additive subgroup of lattice points.

noncomputable def ComplexTorus.proj (L : ComplexLattice) : ℂ →+ ComplexTorus L

The canonical projection ℂ →+ ℂ / L sending a complex number to its class in the complex torus, as an additive group homomorphism.

theorem ComplexTorus.proj_eq_iff (L : ComplexLattice) (z w : ℂ) : (proj L) z = (proj L) w ↔ ∃ v ∈ L.toAddSubgroup, z + v = w

Two complex numbers project to the same class in the complex torus ℂ / L if and only if they differ by an element of the lattice.

@[implicit_reducible]

noncomputable instance ComplexTorus.instInhabited (L : ComplexLattice) : Inhabited (ComplexTorus L)

The complex torus is inhabited by the class of 0.