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) ❙
	
❚