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)