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

theory Elliptic_curve : ?Base = 
  include ?Weierstrass_model ❙
    
  elliptic_curve : type ❙
  
  base_field : elliptic_curve ⟶ field ❙

  weierstrass_model_construction : weierstrass_model ⟶ elliptic_curve ❙

  minimal_Weierstrass_model : elliptic_curve ⟶ weierstrass_model ❙
  
  construction_surjective: {A} ⊦ weierstrass_model_construction (minimal_Weierstrass_model A) ≐ A ❙
  
❚