namespace http://mathhub.info/MitM/core/elliptic_curves ❚
import fnd http://mathhub.info/MitM/Foundation ❚

theory a_Invariants : ?Base =
  include ?Minimal_Weierstrass_model ❙
  a_invariants : elliptic_curve ⟶ (vector ℤ 5) ❘ = [A] a_invariants (minimal_Weierstrass_model A) ❙
❚