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

theory q_Expansion : ?Base =             // illustrates gain in introducing isogeny_class, could talk about modular forms as well ❙
  include ?Isogeny_class ❙
  
  q_expansion: elliptic_curve ⟶ power_series ❙
  q_expansion_factors_through_isogeny_class: {A, B} ⊦ isogeny_equivalence_class A ≐ isogeny_equivalence_class B ⟶ ⊦ q_expansion A ≐ q_expansion B ❙
❚