Commit 3044d7da authored by Dennis Müller's avatar Dennis Müller

update

parent 04043646
......@@ -141,6 +141,7 @@ theory Group : base:?Logic =
order : group ⟶ ℕ ❘ = [g] | fullset (baseset g) |❙
parity : group ⟶ ℤ ❙
solvable : group ⟶ prop ❙
degree : group ⟶ ℤ ❙
psolvable : group ⟶ ℕ+ ⟶ prop ❙
sylow : group ⟶ ℕ+ ⟶ group ❙
......
......@@ -62,6 +62,7 @@ theory Lattice : base:?Logic =
theory lattice_theory : base:?Logic =
include ts:?SetStructures/setstruct_theory ❙
implicit structure meetstruct : ?SemiLattice/semilattice_theory =
universe = `ts:?SetStructures/setstruct_theory?universe ❙
op @ meet ❘ # 1 ⊓ 2 ❙
......@@ -75,7 +76,7 @@ theory Lattice : base:?Logic =
prop_absorption2 : bool ❘ = prop_absorption join meet ❙
axiom_absorption : ⊦ prop_absorption1 ∧ prop_absorption2 ❙
lattice = Mod lattice_theory ❘ role abbreviation
lattice = Mod lattice_theory ❙
theory DistributiveLattice : base:?Logic =
......@@ -89,7 +90,7 @@ theory DistributiveLattice : base:?Logic =
times = meet ❙
distributiveLattice = Mod distributiveLattice_theory ❘ role abbreviation
distributiveLattice = Mod distributiveLattice_theory ❙
theory BoundedLattice : base:?Logic =
......@@ -98,10 +99,10 @@ theory BoundedLattice : base:?Logic =
include ?Lattice/lattice_theory ❙
top : U ❘ # ⊤ ❙
bot : U❘ # ⊥ ❙
axiom_top : ⊦ ∀[a] a ≼ ⊤ ❙ // imported implicitly via SemilatticeIsPOSet ❙
axiom_bot : ⊦ ∀[a] ⊥ ≼ a ❙
// axiom_top : ⊦ ∀[a] a ≼ ⊤ ❙ // imported implicitly via SemilatticeIsPOSet ❙
// axiom_bot : ⊦ ∀[a] ⊥ ≼ a ❙
boundedLattice = Mod boundedLattice_theory ❘ role abbreviation
boundedLattice = Mod boundedLattice_theory ❙
......@@ -113,7 +114,7 @@ theory ComplementedLattice : base:?Logic =
prop_complemented : bool ❘ = ∀[a] ∃[c] comp a c ❙
axiom_complemented : ⊦ prop_complemented ❙
complementedLattice = Mod complementedLattice_theory ❘ role abbreviation
complementedLattice = Mod complementedLattice_theory ❙
theory BooleanAlgebra : base:?Logic =
......@@ -122,5 +123,5 @@ theory BooleanAlgebra : base:?Logic =
include ?ComplementedLattice/complementedLattice_theory ❙
include ?DistributiveLattice/distributiveLattice_theory ❙
booleanalgebra = Mod booleanAlgebra_theory ❘ role abbreviation
booleanalgebra = Mod booleanAlgebra_theory ❙
......@@ -25,6 +25,8 @@ 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 > ❙
orbit : type ❙
theory PermutationGroup : base:?Logic =
......@@ -40,6 +42,7 @@ theory PermutationGroup : base:?Logic =
fromPerm: (List permutation) ⟶ permutationGroup ❙
generators : permutationGroup ⟶ List permutation ❙
dihedralGroup : ℤ ⟶ permutationGroup ❙
theory TransitiveGroupAction : base:?Logic =
......
......@@ -5,12 +5,12 @@ 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.plus) (r.zero) n s ❘ # ∑ 3 ❙
power_seq : {r:ring, n : NAT} r.universe ⟶ r.universe ❘ = [r,n,x] foldL (r.times) (r.one) n ⟨' x | i:n '⟩ ❘ # 3 tothe 2 ❙
polynomial_of : {r : ring, n} (r.universe)^n ⟶ (r.universe) ⟶ (r.universe) ❘ = [r,n,s] [x] ∑ ⟨' ((r.times) (s..i) (x tothe i) ) | i:n '⟩
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] ⟨ ((r.universe) ⟶ (r.universe)) | ([f] ⊦ ∃ [n] exists_seq (r.universe) n [s] f ≐ (polynomial_of s) ) ⟩ ❙
OneDimensionalPolynomialsOver : ring ⟶ type ❘= [r] ⟨ f : (r.universe) ⟶ (r.universe) | ⊦ ∃ [n] exists_seq (r.universe) n [s] f ≐ (polynomial_of s) ⟩ ❙
polynomialRing : ring ⟶ ring ❘ // TODO ❙
......@@ -24,7 +24,7 @@ theory NumberSpaces : base:?Logic =
include ?RationalField ❙
include ?Polynomials ❙
numberField : polynomialRing rationalField ⟶ ring ❙
numberField : (polynomialRing rationalField).universe ⟶ ring ❙
theory RationalPolynomials : base:?Logic =
......@@ -37,4 +37,6 @@ theory RationalPolynomials : base:?Logic =
monomial_con : {r: ring} (List (string × ℕ)) × ℚ ⟶ monomial r ❘ # monomial_con 1 2❙
multi_poly_con : {r : ring} List (monomial r) ⟶ multi_polynomial r ❙
groebner : type ❙
\ No newline at end of file
......@@ -97,7 +97,7 @@ theory Series : base:?Logic =
partialSum : {G : metricMonoid} G^ω ⟶ ℕ ⟶ (G.universe) ❘ # parSum 2 3 ❙
axiom_partialSumBase : {G : metricMonoid} ⊦ ∀[S : G^ω] parSum S 0 ≐ (G.unit) ❙
axiom_partialSumStep : {G : metricMonoid} ⊦ ∀[S : G^ω] ∀[n] parSum S (succ n) ≐ (G.op) (parSum S n) (S (succ n)) ❙
axiom_partialSumStep : {G : metricMonoid} ⊦ ∀[S : G^ω] ∀[n] parSum S (nat_lit_succ n) ≐ (G.op) (parSum S n) (S (nat_lit_succ n)) ❙
prop_convergent : {G : metricMonoid} G^ω ⟶ prop ❘ = [G][S] prop_convergent G ([n] parSum S n) ❙
series : {G : metricMonoid, S: G^ω} dom G ❘ = [G,S] lim (partialSum G S) ❘ # SUM 2 ❙
\ No newline at end of file
......@@ -4,7 +4,7 @@ theory Weierstrass_model : ?Base =
include http://mathhub.info/MitM/smglom/typedsets?Injective ❙
weierstrass_model : type ❙
polynomial_equation : weierstrass_model ⟶ polynomial
polynomial_equation : weierstrass_model ⟶ (polynomial rationalField)
polynomial_equation_injectivity : {A, B} ⊦ polynomial_equation A ≐ polynomial_equation B ⟶ ⊦ A ≐ B ❙
// As the Weierstrass model is really defined by the polynomial_equation, this is really what defines equality. (1) ❙
......
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