Commit 42acf6fa authored by Dennis Müller's avatar Dennis Müller

update

parent 1a3fa565
......@@ -25,6 +25,6 @@ theory HeckeEigenvalues : elliptic_curves?Base =
include ?HilbertNewforms ❙
heckePolynomial : hilbertNewform ⟶ (polynomial rationalField) ❙
heckeEigenvalues : hilbertNewform ⟶ List
heckeEigenvalues : hilbertNewform ⟶ List (polynomial rationalField)
\ No newline at end of file
......@@ -77,6 +77,8 @@ theory RationalField : base:?Logic =
axiom_commutative := forallI [x : ℚ] (forallI [y : ℚ] `arith:?RationalArithmetics?axiom_commutativeTimes x y)
'] ❙ // TODO ugly hack!! ❙
rationalField2 : field ❙
theory RealField : base:?Logic =
......@@ -117,8 +119,8 @@ theory RealVectorspace : base:?Logic =
realVec : kind ❘ = vectorspace realField ❙
realVec1 : realVec ❘ = asVectorspace realField ❘ # ℝ1 ❙
realVec2 : realVec ❘ // = ℝ1 ov ℝ1 ❘ # ℝ2 ❙
realVec3 : realVec ❘ // = ℝ1 ov ℝ2 ❘ # ℝ3 ❙ // takes forever ❙
realVec2 : realVec ❘ // = productspace realField ℝ1 ℝ1 ❘ # ℝ2 ❙
realVec3 : realVec ❘ // = productspace realField ℝ1 ℝ2 ❘ # ℝ3 ❙ // takes forever ❙
// finite_real_vectorspace : pos_lit ⟶ RealVec ❙
......@@ -25,6 +25,7 @@ theory NumberSpaces : base:?Logic =
include ?Polynomials ❙
numberField : (polynomialRing rationalField).universe ⟶ ring ❙
galoisGroup : ring ⟶ group ❙
theory RationalPolynomials : base:?Logic =
......
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