namespace http://mathhub.info/MitM/core/elliptic_curves ❚

theory Complex_multiplication : ?Base =
  include ?Elliptic_curve ❙
  complex_multiplication : elliptic_curve ⟶ prop ❙
❚