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

theory Isogeny_class : ?Base =
  include ?Conductor ❙
    
  isogeny_class: type ❙
  isogeny_equivalence_class: elliptic_curve ⟶ isogeny_class ❙
    
  isogenies_preserve_conductor: {A : elliptic_curve, B:elliptic_curve} ⊦ isogeny_equivalence_class A ≐ isogeny_equivalence_class B ⟶ ⊦ conductor A ≐ conductor B ❙
    // should really be defined as a quotient ❙
❚