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

theory Conductor : ?Base =
  include ?Elliptic_curve ❙
  conductor : elliptic_curve ⟶ ℤ ❙
❚