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

theory Modular_degree : ?Base =
  include ?Conductor ❙
  modular_degree : elliptic_curve ⟶ ℤ ❙
❚