namespace http://mathhub.info/MitM/core/algebra ❚
import base http://mathhub.info/MitM/Foundation ❚
theory HeckeFields : base:?Logic =
include ?Field ❙
degree_over_Q : field ⟶ ℕ ❙
❚
theory HilbertNewforms : base:?Logic =
include ?HeckeFields ❙
hilbertNewform : type ❙
base_field : hilbertNewform ⟶ field ❙
base_field_degree : hilbertNewform ⟶ ℕ ❙
// level_ideal TODO ❙
level_norm : hilbertNewform ⟶ ℤ ❙
dimension : hilbertNewform ⟶ ℕ ❙
❚
theory HeckeEigenvalues : elliptic_curves?Base =
include ?HilbertNewforms ❙
heckePolynomial : hilbertNewform ⟶ (polynomial rationalField) ❙
heckeEigenvalues : hilbertNewform ⟶ List (polynomial rationalField) ❙
❚