def ComplexMultiplication.HasCM (L : ComplexLattice) : Prop

A complex lattice $L$ has complex multiplication if its endomorphism ring contains an element that is not an integer. Equivalently (Definition 12.21), $\mathrm{End}(L) \not\cong \mathbb{Z}$.

def ComplexMultiplication.HasCMBy (L : ComplexLattice) (𝒪 : Subring ℂ) : Prop

The lattice $L$ has complex multiplication by the order $\mathcal{O}$ if $L$ is a proper $\mathcal{O}$-ideal and $\mathcal{O}$ is an order in an imaginary quadratic field.

theorem ComplexMultiplication.hasCM_iff_exists_hasCMBy (L : ComplexLattice) : HasCM L ↔ ∃ (𝒪 : Subring ℂ), HasCMBy L 𝒪

A lattice has complex multiplication iff there exists an order $\mathcal{O}$ in an imaginary quadratic field such that $L$ has CM by $\mathcal{O}$.

theorem ComplexMultiplication.hasCM_iff_isImagQuadOrder (L : ComplexLattice) : HasCM L ↔ ComplexLattice.IsImagQuadOrder L.endomorphismRing

A lattice has complex multiplication iff its endomorphism ring is an order in an imaginary quadratic field.

theorem ComplexMultiplication.not_hasCM_iff_endRing_eq_Z (L : ComplexLattice) : ¬HasCM L ↔ ∀ α ∈ L.endomorphismRing, ∃ (n : ℤ), α = ↑n

A lattice does not have complex multiplication iff every element of its endomorphism ring is an integer; i.e. $\mathrm{End}(L) = \mathbb{Z}$.