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

import base http://mathhub.info/MitM/Foundation ❚

theory Polynomials : base:?Logic =
	include ☞base:?Sequences ❙
	include ?Ring ❙
	finiteSum : {r:ring, n} (r.universe)^n ⟶ (r.universe) ❘ = [r,n,s] foldL (r.rplus) (r.rzero) n s  ❘ # ∑ 3 ❙
	power_seq : {r:ring, n : NAT} r.universe ⟶ r.universe ❘ = [r,n,x] foldL (r.rtimes) (r.rone) n ⟨' x | i:n '⟩ ❘ # 3 tothe 2 ❙
	polynomial_of : {r : ring, n} (r.universe)^n ⟶ (r.universe) ⟶ (r.universe) ❘ = [r,n,s] [x] ∑ ⟨' ((r.rtimes) (s..i) (x tothe i) ) | i:n '⟩
		❘ # polynomial_of 3 ❙ 
	
	OneDimensionalPolynomialsOver : ring ⟶ type ❘= [r] ⟨ f : (r.universe) ⟶ (r.universe) | ⊦ ∃ [n] exists_seq (r.universe) n [s] f ≐ (polynomial_of s)  ⟩ ❙
	
	polynomialRing : ring ⟶ ring ❘ // TODO ❙
	
	polynomial : ring ⟶ type ❘ = [r] (polynomialRing r).universe ❙
	
	multi_polynomial : ring ⟶ type ❙
	monomial : {r : ring} type ❘ # monomial 1❙
❚

theory NumberSpaces : base:?Logic =
	include ?RationalField ❙
	include ?Polynomials ❙
	
	numberField : (polynomialRing rationalField).universe ⟶ ring ❙
	galoisGroup : ring ⟶ group ❙
❚

theory RationalPolynomials : base:?Logic =
	include ?Polynomials ❙
	include ☞base:?Lists ❙
	include algebra?RationalField ❙
	include ☞base:?ProductTypes ❙
	
	poly_con : {r : ring} string ⟶ List ℚ ⟶ polynomial r ❘ // = [n,s] polynomial_of s ❙
	
	monomial_con : {r: ring} (List (string × ℕ)) × ℚ ⟶ monomial r ❘ # monomial_con 1 2❙
	multi_poly_con : {r : ring} List (monomial r) ⟶ multi_polynomial r ❘ # mpoly 2 ❙
	
	// x1 =  "x1" ❙
	// x2 = "x2" ❙
	// test1 = ⟨ x1 , 1 ⟩ ❙
	// m1 = monomial_con rationalField2 ⟨  (⟨ x1 , 1 ⟩ ++ nil) , 3 ⟩ ❙
	// m2 = monomial_con rationalField2 ⟨ (⟨ x2, 1⟩ ++ nil),2⟩ ❙
	// p = mpoly (ls m1,m2) ❙
	
	groebner : {r : ring} List (multi_polynomial r) ⟶ List (multi_polynomial r) ❘ # groebner 2 ❙
❚