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

theory Discriminant : ?Base = 
  include ?Minimal_Weierstrass_model ❙
  // include ?Weierstrass_model ❙
  discriminant : elliptic_curve ⟶ ℤ ❘ = [A] discriminant (minimal_Weierstrass_model A) ❙
❚