Commit 8b5bc7f3 authored by Dennis Müller's avatar Dennis Müller

update

parent dddc7758
......@@ -13,4 +13,21 @@ theory Polynomials : base:?Logic =
OneDimensionalPolynomialsOver : ring ⟶ type ❘= [r] ⟨ ((r.universe) ⟶ (r.universe)) | ([f] ⊦ ∃ [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 RationalPolynomials : base:?Logic =
include ?Polynomials ❙
include base:?Lists ❙
include algebra?RationalField ❙
include base:?ProductType ❙
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 ❙
\ No newline at end of file
......@@ -7,10 +7,6 @@ theory Base : base:?Logic =
include num:?IntegerArithmetics ❙
include algebra?Field ❙
include base:?Matrices ❙
include base:?Lists ❙
include algebra?Polynomials ❙
include algebra?RationalField ❙
include algebra?RationalPolynomials ❙
power_series : type ❙
polynomial : ring ⟶ type ❘ = [r] (polynomialRing r).universe ❙
poly_con : {r : ring} string ⟶ List ℚ ⟶ polynomial r ❘ // = [n,s] polynomial_of s ❙
\ 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