Commit 3c5019fd authored by Dennis Müller's avatar Dennis Müller

Merge branch 'devel' into Sven

parents 3b26b595 9c5dd948
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="AbelianGroup" base="http://mathhub.info/MitM/smglom/algebra" meta="http://mathhub.info/MitM/Foundation?Logic"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#5258.147.0:5504.156.0"/></metadata><import from="http://mathhub.info/MitM/smglom/algebra?Group"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#5295.148.1:5308.148.14"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><theory name="abeliangroup_theory" base="http://mathhub.info/MitM/smglom/algebra" meta="http://mathhub.info/MitM/Foundation?Logic">
<metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#5314.150.1:5438.153.1"/></metadata><import from="http://mathhub.info/MitM/smglom/algebra?Group/group_theory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#5359.151.2:5385.151.28"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><constant name="axiom_commutative">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#5393.152.2:5435.152.44"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#5413.152.22:5433.152.42"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/Foundation" module="Logic" name="ded"></om:OMS><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#5415.152.24:5433.152.42"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="OperationProps" name="prop_commutative"></om:OMS><om:OMS base="http://mathhub.info/MitM/smglom/typedsets" module="SetStructures/setstruct_theory" name="universe"></om:OMS><om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="Magma/magma_theory" name="op"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#5432.152.41:5433.152.42"/></metadata></om:OMS>
</om:OMA>
</om:OMA></om:OMOBJ></type>
</constant>
</theory><constant name="abeliangroup" role="abbreviation">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#5441.154.1:5500.154.60"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#5456.154.16:5478.154.38"/></metadata>
<om:OMS base="http://gl.mathhub.info/MMT/LFX/Records" module="Symbols" name="ModelsOfUnary"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="AbelianGroup/abeliangroup_theory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#5460.154.20:5478.154.38"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></definition>
</constant></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Band" base="http://mathhub.info/MitM/smglom/algebra" meta="http://mathhub.info/MitM/Foundation?Logic"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#418.14.0:656.21.0"/></metadata><import from="http://mathhub.info/MitM/smglom/algebra?IdempotentMagma"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#449.15.2:473.15.26"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata></import><theory name="band_theory" base="http://mathhub.info/MitM/smglom/algebra" meta="http://mathhub.info/MitM/Foundation?Logic">
<metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#477.16.2:608.19.2"/></metadata><import from="http://mathhub.info/MitM/smglom/algebra?IdempotentMagma/idempotent_theory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#518.17.5:559.17.46"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><import from="http://mathhub.info/MitM/smglom/algebra?SemiGroup/semigroup_theory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#568.18.5:602.18.39"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import>
</theory><constant name="band" role="abbreviation">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#612.20.2:654.20.44"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#619.20.9:633.20.23"/></metadata>
<om:OMS base="http://gl.mathhub.info/MMT/LFX/Records" module="Symbols" name="ModelsOfUnary"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="Band/band_theory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#623.20.13:633.20.23"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></definition>
</constant></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="BooleanAlgebra" base="http://mathhub.info/MitM/smglom/algebra" meta="http://mathhub.info/MitM/Foundation?Logic"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA>
<om:OMS base="http://gl.mathhub.info/MMT/LFX/TypedHierarchy" module="Symbols" name="TypeLevel"></om:OMS>
<om:OMLIT type="http://mathhub.info/MitM/Foundation?Literals?nat_lit" value="100"/>
</om:OMA></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#4624.137.0:4939.144.0"/></metadata><import from="http://mathhub.info/MitM/smglom/algebra?ComplementedLattice"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#4664.138.2:4692.138.30"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA>
<om:OMS base="http://gl.mathhub.info/MMT/LFX/TypedHierarchy" module="Symbols" name="TypeLevel"></om:OMS>
<om:OMLIT type="http://mathhub.info/MitM/Foundation?Literals?nat_lit" value="100"/>
</om:OMA></om:OMOBJ></meta></metadata></import><theory name="booleanAlgebra_theory" base="http://mathhub.info/MitM/smglom/algebra" meta="http://mathhub.info/MitM/Foundation?Logic">
<metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#4696.139.2:4870.142.2"/></metadata><import from="http://mathhub.info/MitM/smglom/algebra?ComplementedLattice/complementedLattice_theory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#4747.140.5:4801.140.59"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><import from="http://mathhub.info/MitM/smglom/algebra?DistributiveLattice/distributiveLattice_theory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#4810.141.5:4864.141.59"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import>
</theory><constant name="booleanalgebra" role="abbreviation">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#4874.143.2:4937.143.65"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#4891.143.19:4915.143.43"/></metadata>
<om:OMS base="http://gl.mathhub.info/MMT/LFX/Records" module="Symbols" name="ModelsOfUnary"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="BooleanAlgebra/booleanAlgebra_theory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#4895.143.23:4915.143.43"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></definition>
</constant></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="CancellativeMagma" base="http://mathhub.info/MitM/smglom/algebra" meta="http://mathhub.info/MitM/Foundation?Logic"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3123.72.0:3660.86.0"/></metadata><import from="http://mathhub.info/MitM/smglom/algebra?Magma"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3166.73.1:3179.73.14"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata></import><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3183.74.0:3262.74.79"/></metadata>MiKo: use this to make a view into quasisgroup Theory: they are cancellative</opaque><theory name="cancellativemagma_theory" base="http://mathhub.info/MitM/smglom/algebra" meta="http://mathhub.info/MitM/Foundation?Logic">
<metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3266.75.2:3463.79.2"/></metadata><import from="http://mathhub.info/MitM/smglom/algebra?Magma/magma_theory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3316.76.2:3342.76.28"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><constant name="axiom_leftCancellative">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3348.77.2:3401.77.55"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3373.77.27:3398.77.52"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/Foundation" module="Logic" name="ded"></om:OMS><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3375.77.29:3398.77.52"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="OperationProps" name="prop_leftCancellative"></om:OMS><om:OMS base="http://mathhub.info/MitM/smglom/typedsets" module="SetStructures/setstruct_theory" name="universe"></om:OMS><om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="Magma/magma_theory" name="op"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3397.77.51:3398.77.52"/></metadata></om:OMS>
</om:OMA>
</om:OMA></om:OMOBJ></type>
</constant><constant name="axiom_rightCancellative">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3405.78.2:3459.78.56"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3431.78.28:3457.78.54"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/Foundation" module="Logic" name="ded"></om:OMS><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3433.78.30:3457.78.54"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="OperationProps" name="prop_rightCancellative"></om:OMS><om:OMS base="http://mathhub.info/MitM/smglom/typedsets" module="SetStructures/setstruct_theory" name="universe"></om:OMS><om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="Magma/magma_theory" name="op"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3456.78.53:3457.78.54"/></metadata></om:OMS>
</om:OMA>
</om:OMA></om:OMOBJ></type>
</constant>
</theory><constant name="cancellativemagma" role="abbreviation">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3468.81.2:3537.81.71"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3488.81.22:3515.81.49"/></metadata>
<om:OMS base="http://gl.mathhub.info/MMT/LFX/Records" module="Symbols" name="ModelsOfUnary"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="CancellativeMagma/cancellativemagma_theory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3492.81.26:3515.81.49"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></definition>
</constant><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3544.83.2:3585.83.43"/></metadata>MiKo: how to express the definitions?</opaque><constant name="leftCancellative">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3589.84.2:3621.84.34"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3608.84.21:3619.84.32"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="Magma" name="magma"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3608.84.21:3612.84.25"/></metadata></om:OMS><om:OMS base="http://mathhub.info/MitM/Foundation" module="Logic" name="prop"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3616.84.29:3619.84.32"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
</constant><constant name="rightCancellative">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3625.85.2:3658.85.35"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3645.85.22:3656.85.33"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="Magma" name="magma"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3645.85.22:3649.85.26"/></metadata></om:OMS><om:OMS base="http://mathhub.info/MitM/Foundation" module="Logic" name="prop"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#3653.85.30:3656.85.33"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
</constant></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="DistributiveLattice" base="http://mathhub.info/MitM/smglom/algebra" meta="http://mathhub.info/MitM/Foundation?Logic"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA>
<om:OMS base="http://gl.mathhub.info/MMT/LFX/TypedHierarchy" module="Symbols" name="TypeLevel"></om:OMS>
<om:OMLIT type="http://mathhub.info/MitM/Foundation?Literals?nat_lit" value="100"/>
</om:OMA></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3425.99.0:3794.111.0"/></metadata><import from="http://mathhub.info/MitM/smglom/algebra?Lattice"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3469.100.1:3484.100.16"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA>
<om:OMS base="http://gl.mathhub.info/MMT/LFX/TypedHierarchy" module="Symbols" name="TypeLevel"></om:OMS>
<om:OMLIT type="http://mathhub.info/MitM/Foundation?Literals?nat_lit" value="100"/>
</om:OMA></om:OMOBJ></meta></metadata></import><import from="http://mathhub.info/MitM/smglom/algebra?Ringoid"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3489.101.1:3504.101.16"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA>
<om:OMS base="http://gl.mathhub.info/MMT/LFX/TypedHierarchy" module="Symbols" name="TypeLevel"></om:OMS>
<om:OMLIT type="http://mathhub.info/MitM/Foundation?Literals?nat_lit" value="100"/>
</om:OMA></om:OMOBJ></meta></metadata></import><theory name="distributiveLattice_theory" base="http://mathhub.info/MitM/smglom/algebra" meta="http://mathhub.info/MitM/Foundation?Logic">
<metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3510.102.2:3715.109.2"/></metadata><import from="http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3566.103.5:3596.103.35"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><import name="ringoid" from="http://mathhub.info/MitM/smglom/algebra?Ringoid/ringoid_theory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3605.104.5:3711.108.5"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata><constant name="[http://mathhub.info/MitM/smglom/algebra?Ringoid/ringoid_theory]/addition/[http://mathhub.info/MitM/smglom/typedsets?SetStructures/setstruct_theory]/universe">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3657.105.6:3663.105.12"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://mathhub.info/MitM/smglom/typedsets" module="SetStructures/setstruct_theory" name="universe"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3661.105.10:3661.105.10"/></metadata></om:OMS></om:OMOBJ></definition>
</constant><constant name="[http://mathhub.info/MitM/smglom/algebra?Ringoid/ringoid_theory]/addition/op">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3671.106.6:3683.106.18"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#1740.24.7:1748.24.15"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/typedsets" module="SetStructures/setstruct_theory" name="universe"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3661.105.10:3661.105.10"/></metadata></om:OMS><om:OMS base="http://mathhub.info/MitM/smglom/typedsets" module="SetStructures/setstruct_theory" name="universe"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3661.105.10:3661.105.10"/></metadata></om:OMS><om:OMS base="http://mathhub.info/MitM/smglom/typedsets" module="SetStructures/setstruct_theory" name="universe"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3661.105.10:3661.105.10"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="Lattice/lattice_theory" name="joinstruct/[http://mathhub.info/MitM/smglom/algebra?Magma/magma_theory]/op"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3678.106.13:3681.106.16"/></metadata></om:OMS></om:OMOBJ></definition>
</constant><constant name="[http://mathhub.info/MitM/smglom/algebra?Ringoid/ringoid_theory]/multiplication/op">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3691.107.6:3704.107.19"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#1740.24.7:1748.24.15"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/typedsets" module="SetStructures/setstruct_theory" name="universe"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3661.105.10:3661.105.10"/></metadata></om:OMS><om:OMS base="http://mathhub.info/MitM/smglom/typedsets" module="SetStructures/setstruct_theory" name="universe"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3661.105.10:3661.105.10"/></metadata></om:OMS><om:OMS base="http://mathhub.info/MitM/smglom/typedsets" module="SetStructures/setstruct_theory" name="universe"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3661.105.10:3661.105.10"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="Lattice/lattice_theory" name="meetstruct/[http://mathhub.info/MitM/smglom/algebra?Magma/magma_theory]/op"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3699.107.14:3702.107.17"/></metadata></om:OMS></om:OMOBJ></definition>
</constant></import>
</theory><constant name="distributiveLattice" role="abbreviation">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3719.110.2:3792.110.75"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3741.110.24:3770.110.53"/></metadata>
<om:OMS base="http://gl.mathhub.info/MMT/LFX/Records" module="Symbols" name="ModelsOfUnary"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="DistributiveLattice/distributiveLattice_theory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3745.110.28:3770.110.53"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></definition>
</constant></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="HeckeEigenvalues" base="http://mathhub.info/MitM/smglom/algebra" meta="http://mathhub.info/MitM/smglom/elliptic_curves?Base"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#470.23.0:653.28.0"/></metadata><import from="http://mathhub.info/MitM/smglom/algebra?HilbertNewforms"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#520.24.1:543.24.24"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><constant name="heckePolynomial">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#550.26.1:596.26.47"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#568.26.19:594.26.45"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="HilbertNewforms" name="hilbertNewform"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#568.26.19:581.26.32"/></metadata></om:OMS><om:OMS base="http://mathhub.info/MitM/smglom/elliptic_curves" module="Base" name="polynomial"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#585.26.36:594.26.45"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
</constant><constant name="heckeEigenvalues">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#599.27.1:651.27.53"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#618.27.20:649.27.51"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="HilbertNewforms" name="hilbertNewform"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#618.27.20:631.27.33"/></metadata></om:OMS><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#635.27.37:649.27.51"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/Foundation" module="Lists" name="list"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#635.27.37:638.27.40"/></metadata></om:OMS><om:OMS base="http://mathhub.info/MitM/smglom/elliptic_curves" module="Base" name="polynomial"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#640.27.42:649.27.51"/></metadata></om:OMS>
</om:OMA>
</om:OMA></om:OMOBJ></type>
</constant></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="HeckeFields" base="http://mathhub.info/MitM/smglom/algebra" meta="http://mathhub.info/MitM/Foundation?Logic"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#104.4.0:188.8.0"/></metadata><import from="http://mathhub.info/MitM/smglom/algebra?Field"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#140.5.1:153.5.14"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><constant name="degree_over_Q">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#160.7.1:186.7.27"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#176.7.17:184.7.25"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="Field" name="field"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#176.7.17:180.7.21"/></metadata></om:OMS><om:OMS base="http://mathhub.info/MitM/Foundation" module="NatLiterals" name="nat_lit"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#184.7.25:184.7.25"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
</constant></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="HilbertNewforms" base="http://mathhub.info/MitM/smglom/algebra" meta="http://mathhub.info/MitM/Foundation?Logic"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#191.10.0:467.21.0"/></metadata><import from="http://mathhub.info/MitM/smglom/algebra?HeckeFields"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#231.11.1:250.11.20"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><constant name="hilbertNewform">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#256.12.2:278.12.24"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#273.12.19:276.12.22"/></metadata></om:OMS></om:OMOBJ></type>
</constant><constant name="base_field">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#285.14.2:321.14.38"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#298.14.15:319.14.36"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="HilbertNewforms" name="hilbertNewform"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#298.14.15:311.14.28"/></metadata></om:OMS><om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="Field" name="field"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#315.14.32:319.14.36"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
</constant><constant name="base_field_degree">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#325.15.2:364.15.41"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#345.15.22:362.15.39"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="HilbertNewforms" name="hilbertNewform"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#345.15.22:358.15.35"/></metadata></om:OMS><om:OMS base="http://mathhub.info/MitM/Foundation" module="NatLiterals" name="nat_lit"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#362.15.39:362.15.39"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
</constant><constant name="level_norm">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#395.18.2:427.18.34"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#408.18.15:425.18.32"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="HilbertNewforms" name="hilbertNewform"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#408.18.15:421.18.28"/></metadata></om:OMS><om:OMS base="http://mathhub.info/MitM/Foundation" module="IntLiterals" name="int_lit"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#425.18.32:425.18.32"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
</constant><constant name="dimension">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#434.20.2:465.20.33"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#446.20.14:463.20.31"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="HilbertNewforms" name="hilbertNewform"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#446.20.14:459.20.27"/></metadata></om:OMS><om:OMS base="http://mathhub.info/MitM/Foundation" module="NatLiterals" name="nat_lit"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/hecke.mmt#463.20.31:463.20.31"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
</constant></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="IdempotentMagma" base="http://mathhub.info/MitM/smglom/algebra" meta="http://mathhub.info/MitM/Foundation?Logic"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#157.4.0:415.12.0"/></metadata><import from="http://mathhub.info/MitM/smglom/algebra?OperationProps"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#199.5.2:221.5.24"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata></import><theory name="idempotent_theory" base="http://mathhub.info/MitM/smglom/algebra" meta="http://mathhub.info/MitM/Foundation?Logic">
<metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#230.7.2:349.10.2"/></metadata><import from="http://mathhub.info/MitM/smglom/algebra?Magma/magma_theory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#273.8.2:299.8.28"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><constant name="axiom_idempotent">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#305.9.2:345.9.42"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#324.9.21:343.9.40"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/Foundation" module="Logic" name="ded"></om:OMS><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#326.9.23:343.9.40"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="OperationProps" name="prop_idempotent"></om:OMS><om:OMS base="http://mathhub.info/MitM/smglom/typedsets" module="SetStructures/setstruct_theory" name="universe"></om:OMS><om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="Magma/magma_theory" name="op"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#342.9.39:343.9.40"/></metadata></om:OMS>
</om:OMA>
</om:OMA></om:OMOBJ></type>
</constant>
</theory><constant name="idempotentMagma" role="abbreviation">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#353.11.2:413.11.62"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#371.11.20:391.11.40"/></metadata>
<om:OMS base="http://gl.mathhub.info/MMT/LFX/Records" module="Symbols" name="ModelsOfUnary"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="IdempotentMagma/idempotent_theory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#375.11.24:391.11.40"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></definition>
</constant></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Monoid" base="http://mathhub.info/MitM/smglom/algebra" meta="http://mathhub.info/MitM/Foundation?Logic"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#4323.108.0:4564.118.0"/></metadata><import from="http://mathhub.info/MitM/smglom/algebra?SemiGroup"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#4354.109.1:4371.109.18"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata></import><import from="http://mathhub.info/MitM/smglom/algebra?Unital"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#4376.110.1:4390.110.15"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata></import><theory name="monoid_theory" base="http://mathhub.info/MitM/smglom/algebra" meta="http://mathhub.info/MitM/Foundation?Logic">
<metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#4397.112.1:4509.115.1"/></metadata><import from="http://mathhub.info/MitM/smglom/algebra?SemiGroup/semigroup_theory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#4436.113.2:4470.113.36"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><import from="http://mathhub.info/MitM/smglom/algebra?Unital/unital_theory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#4476.114.2:4504.114.30"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import>
</theory><constant name="monoid" role="abbreviation">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#4512.116.1:4559.116.48"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#4521.116.10:4537.116.26"/></metadata>
<om:OMS base="http://gl.mathhub.info/MMT/LFX/Records" module="Symbols" name="ModelsOfUnary"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="Monoid/monoid_theory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#4525.116.14:4537.116.26"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></definition>
</constant></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="RealVectorspace" base="http://mathhub.info/MitM/smglom/algebra" meta="http://mathhub.info/MitM/Foundation?Logic"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA>
<om:OMS base="http://gl.mathhub.info/MMT/LFX/TypedHierarchy" module="Symbols" name="TypeLevel"></om:OMS>
<om:OMLIT type="http://mathhub.info/MitM/Foundation?Literals?nat_lit" value="100"/>
</om:OMA></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5312.112.0:5699.122.0"/></metadata><import from="http://mathhub.info/MitM/smglom/algebra?Vectorspace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5352.113.1:5371.113.20"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><import from="http://mathhub.info/MitM/smglom/algebra?RealField"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5376.114.1:5393.114.18"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><import from="http://mathhub.info/MitM/smglom/algebra?Productspace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5398.115.1:5418.115.21"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA>
<om:OMS base="http://gl.mathhub.info/MMT/LFX/TypedHierarchy" module="Symbols" name="TypeLevel"></om:OMS>
<om:OMLIT type="http://mathhub.info/MitM/Foundation?Literals?nat_lit" value="100"/>
</om:OMA></om:OMOBJ></meta></metadata></import><constant name="realVec">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5425.117.1:5466.117.42"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5435.117.11:5438.117.14"/></metadata></om:OMS></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5480.118.12:5486.118.18"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="Vectorspace" name="vectorspace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5444.117.20:5454.117.30"/></metadata></om:OMS><om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="RealField" name="realField"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5456.117.32:5464.117.40"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></definition>
</constant><constant name="realVec1">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5469.118.1:5523.118.55"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="RealVectorspace" name="realVec"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5480.118.12:5486.118.18"/></metadata></om:OMS></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5492.118.24:5514.118.46"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="Vectorspace" name="asVectorspace"></om:OMS><om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="RealField" name="realField"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5506.118.38:5514.118.46"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></definition>
<notations><notation dimension="1" precedence="0" fixity="mixfix" arguments="ℝ1"> <scope languages="" priority="0"/> </notation></notations>
</constant><constant name="realVec2">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5526.119.1:5585.119.60"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="RealVectorspace" name="realVec"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5537.119.12:5543.119.18"/></metadata></om:OMS></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5549.119.24:5576.119.51"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="Productspace" name="productspace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5549.119.24:5560.119.35"/></metadata></om:OMS><om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="RealField" name="realField"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5562.119.37:5570.119.45"/></metadata></om:OMS><om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="RealVectorspace" name="realVec1"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5572.119.47:5573.119.48"/></metadata></om:OMS><om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="RealVectorspace" name="realVec1"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5575.119.50:5576.119.51"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></definition>
<notations><notation dimension="1" precedence="0" fixity="mixfix" arguments="ℝ2"> <scope languages="" priority="0"/> </notation></notations>
</constant><constant name="realVec3">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5588.120.1:5647.120.60"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="RealVectorspace" name="realVec"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5599.120.12:5605.120.18"/></metadata></om:OMS></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5611.120.24:5638.120.51"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="Productspace" name="productspace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5611.120.24:5622.120.35"/></metadata></om:OMS><om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="RealField" name="realField"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5624.120.37:5632.120.45"/></metadata></om:OMS><om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="RealVectorspace" name="realVec1"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5634.120.47:5635.120.48"/></metadata></om:OMS><om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="RealVectorspace" name="realVec2"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/numberspaces.mmt#5637.120.50:5638.120.51"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></definition>
<notations><notation dimension="1" precedence="0" fixity="mixfix" arguments="ℝ3"> <scope languages="" priority="0"/> </notation></notations>
</constant></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="SemiGroup" base="http://mathhub.info/MitM/smglom/algebra" meta="http://mathhub.info/MitM/Foundation?Logic"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#2005.32.0:2235.40.0"/></metadata><import from="http://mathhub.info/MitM/smglom/algebra?Magma"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#2039.33.1:2052.33.14"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata></import><theory name="semigroup_theory" base="http://mathhub.info/MitM/smglom/algebra" meta="http://mathhub.info/MitM/Foundation?Logic">
<metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#2058.35.1:2177.38.1"/></metadata><import from="http://mathhub.info/MitM/smglom/algebra?Magma/magma_theory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#2100.36.2:2126.36.28"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><constant name="axiom_associative">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#2132.37.2:2174.37.44"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#2152.37.22:2172.37.42"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/Foundation" module="Logic" name="ded"></om:OMS><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#2154.37.24:2172.37.42"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="OperationProps" name="prop_associative"></om:OMS><om:OMS base="http://mathhub.info/MitM/smglom/typedsets" module="SetStructures/setstruct_theory" name="universe"></om:OMS><om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="Magma/magma_theory" name="op"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#2171.37.41:2172.37.42"/></metadata></om:OMS>
</om:OMA>
</om:OMA></om:OMOBJ></type>
</constant>
</theory><constant name="semigroup" role="abbreviation">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#2180.39.1:2233.39.54"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#2192.39.13:2211.39.32"/></metadata>
<om:OMS base="http://gl.mathhub.info/MMT/LFX/Records" module="Symbols" name="ModelsOfUnary"></om:OMS>
<om:OMS base="http://mathhub.info/MitM/smglom/algebra" module="SemiGroup/semigroup_theory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/basics.mmt#2196.39.17:2211.39.32"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></definition>
</constant></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="StabilizerChain" base="http://mathhub.info/MitM/smglom/algebra/groups" meta="http://mathhub.info/MitM/Foundation?Logic"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA>
<om:OMS base="http://gl.mathhub.info/MMT/LFX/TypedHierarchy" module="Symbols" name="TypeLevel"></om:OMS>
<om:OMLIT type="http://mathhub.info/MitM/Foundation?Literals?nat_lit" value="100"/>
</om:OMA></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/StabilizerChain.mmt#220.6.0:510.16.0"/></metadata><import from="http://mathhub.info/MitM/smglom/algebra/groups?PermutationGroups"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/StabilizerChain.mmt#259.7.1:284.7.26"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA>
<om:OMS base="http://gl.mathhub.info/MMT/LFX/TypedHierarchy" module="Symbols" name="TypeLevel"></om:OMS>
<om:OMLIT type="http://mathhub.info/MitM/Foundation?Literals?nat_lit" value="100"/>
</om:OMA></om:OMOBJ></meta></metadata></import><import from="http://mathhub.info/MitM/smglom/algebra/groups?GroupActions"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/StabilizerChain.mmt#289.8.1:309.8.21"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA>
<om:OMS base="http://gl.mathhub.info/MMT/LFX/TypedHierarchy" module="Symbols" name="TypeLevel"></om:OMS>
<om:OMLIT type="http://mathhub.info/MitM/Foundation?Literals?nat_lit" value="100"/>
</om:OMA></om:OMOBJ></meta></metadata></import><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/StabilizerChain.mmt#316.10.1:362.10.47"/></metadata>A step in a Schreier-Sims Stabiliser Chain</opaque></theory></omdoc>
\ No newline at end of file