Commit 3671555e authored by Dennis Müller's avatar Dennis Müller

update

parent c850a198
......@@ -77,7 +77,7 @@ theory RationalField : base:?Logic =
axiom_commutative := forallI [x : ℚ] (forallI [y : ℚ] `arith:?RationalArithmetics?axiom_commutativeTimes x y)
'] ❙ // TODO ugly hack!! ❙
rationalField2 : field ❙
rationalField2 : field ❘ # IntegerRing
......
......@@ -27,7 +27,9 @@ theory GroupAction : base:?Logic =
groupAction = Mod groupAction_theory❙
outer_notation : {GX : groupAction, g : dom GX, x : GX.X} GX.X ❘= [GX,g,x] ((GX.phi) g) x ❘# 2 < 3 > ❙
polynomialOrbit : type ❙
include ../algebra?RationalPolynomials ❙
polynomialOrbit : {r : ring} group ⟶ multi_polynomial r ⟶ List (multi_polynomial r) ❘ # orbit 2 3 ❙
theory PermutationGroup : base:?Logic =
......
......@@ -37,7 +37,14 @@ theory RationalPolynomials : base:?Logic =
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 ❙
multi_poly_con : {r : ring} List (monomial r) ⟶ multi_polynomial r ❘ # mpoly 2
groebner : type ❙
// 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 ❙
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment