namespace http://mathhub.info/MitM/core/elliptic_curves ❚
import lmfdb http://www.lmfdb.org/omf ❚

theory Elliptic_curve_toolchest : ?Base = 
    include ?Modular_degree ❙
    include ?a_Invariants ❙
    include ?Discriminant ❙
    // include ec_2_adic_data ❙
    // include ec_padic_data ❙

    // include lmfdb:?LMFDB_label ❙
    // include lmfdb:?Cremona_label ❙          
    // clash in some names, such as conductor_component, although domains are different
    // Dennis: Should be fine; Florian massively improved disambiguation at some point :) ❙

    include ?Isogeny_class ❙
    include ?q_Expansion ❙
    include ?Complex_multiplication ❙
    include ?Conductor ❙
    
    // include minimal_Weierstrass_model ❙ 
    // discriminant makes this redundant
    // Dennis: true; commented it out  ❙
❚