Commit dddc7758 authored by Dennis Müller's avatar Dennis Müller

update

parent 2ae47da9
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/algebra/bands.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/bands.mmt#0.0.0:2292.82.0"/></metadata><mref name="[http://mathhub.info/MitM/smglom/algebra?IdempotentMagma]" target="http://mathhub.info/MitM/smglom/algebra?IdempotentMagma"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/bands.mmt#103.3.0:124.3.21"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra/bands?Band]" target="http://mathhub.info/MitM/smglom/algebra/bands?Band"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/bands.mmt#453.16.0:463.16.10"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra/bands?Regular]" target="http://mathhub.info/MitM/smglom/algebra/bands?Regular"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/bands.mmt#727.26.0:740.26.13"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal]" target="http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/bands.mmt#925.36.0:941.36.16"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra/bands?RightNormal]" target="http://mathhub.info/MitM/smglom/algebra/bands?RightNormal"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/bands.mmt#1309.50.0:1326.50.17"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra/bands?Normal]" target="http://mathhub.info/MitM/smglom/algebra/bands?Normal"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/bands.mmt#1698.64.0:1710.64.12"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/algebra/computational_groups/ActingOnPolynomials.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/ActingOnPolynomials.mmt#0.0.0:682.15.0"/></metadata><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/ActingOnPolynomials.mmt#158.5.0:682.15.0"/></metadata><scope>This obviously doesn't type check yet ❙
theory ActionOnPolynomials : fnd:?Logic =
include ?SymmetricGroup
include ?GroupAction
/T I think this is what I would want
though it is entirely unclear to me right now
how one would encode an induced action (if at all)❙
symmetricGroupActionOnPolynomials : type = <scope>vars : type</scope> rightGroupActions (SymmetricGroup vars) (Polynomials vars) ❙
groupActionOnPolynomials : type = <scope>vars : type</scope> <scope>act : rightGroupActions G vars</scope> rightGroupActions G (Polynomials vars) ❙</scope></opaque></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/algebra/computational_groups/GroupActions.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/GroupActions.mmt#0.0.0:1766.37.0"/></metadata><mref name="[http://mathhub.info/MitM/smglom/algebra/groups?GroupActions]" target="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/GroupActions.mmt#210.6.0:228.6.18"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/algebra/computational_groups/Groups.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/Groups.mmt#0.0.0:3018.88.0"/></metadata><mref name="[http://mathhub.info/MitM/smglom/algebra/groups?Subgroups]" target="http://mathhub.info/MitM/smglom/algebra/groups?Subgroups"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/Groups.mmt#210.6.0:225.6.15"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/algebra/computational_groups/PermutationGroups.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/PermutationGroups.mmt#0.0.0:817.24.0"/></metadata><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/PermutationGroups.mmt#221.7.0:278.7.57"/></metadata>Permutation groups are subgroups of SymmetricGroup(Ω)</opaque><mref name="[http://mathhub.info/MitM/smglom/algebra/groups?PermutationGroups]" target="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/PermutationGroups.mmt#280.8.0:303.8.23"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra/groups?PermutationGroupsN]" target="http://mathhub.info/MitM/smglom/algebra/groups?PermutationGroupsN"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/PermutationGroups.mmt#546.17.0:570.17.24"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/algebra/computational_groups/StabilizerChain.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/StabilizerChain.mmt#0.0.0:510.16.0"/></metadata><mref name="[http://mathhub.info/MitM/smglom/algebra/groups?StabilizerChain]" target="http://mathhub.info/MitM/smglom/algebra/groups?StabilizerChain"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/StabilizerChain.mmt#220.6.0:241.6.21"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/algebra/computational_groups/SymmetricGroups.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/SymmetricGroups.mmt#0.0.0:1165.37.0"/></metadata><mref name="[http://mathhub.info/MitM/smglom/algebra/groups?SymmetricGroup]" target="http://mathhub.info/MitM/smglom/algebra/groups?SymmetricGroup"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/SymmetricGroups.mmt#220.6.0:240.6.20"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra/groups?SymmetricGroupOfN]" target="http://mathhub.info/MitM/smglom/algebra/groups?SymmetricGroupOfN"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/SymmetricGroups.mmt#984.32.0:1007.32.23"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.mmt#0.0.0:5184.167.0"/></metadata><mref name="[http://mathhub.info/MitM/groups?SylowSubgroup]" target="http://mathhub.info/MitM/groups?SylowSubgroup"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.mmt#95.4.0:114.4.19"/></metadata></mref><mref name="[http://mathhub.info/MitM/groups?left_coset]" target="http://mathhub.info/MitM/groups?left_coset"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.mmt#463.20.0:479.20.16"/></metadata></mref><mref name="[http://mathhub.info/MitM/groups?normal_subgroup]" target="http://mathhub.info/MitM/groups?normal_subgroup"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.mmt#742.30.0:763.30.21"/></metadata></mref><mref name="[http://mathhub.info/MitM/groups?group_homomorphism]" target="http://mathhub.info/MitM/groups?group_homomorphism"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.mmt#1409.55.0:1433.55.24"/></metadata></mref><mref name="[http://mathhub.info/MitM/groups?group_action]" target="http://mathhub.info/MitM/groups?group_action"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.mmt#1738.67.0:1756.67.18"/></metadata></mref><mref name="[http://mathhub.info/MitM/groups?permutation_representation]" target="http://mathhub.info/MitM/groups?permutation_representation"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.mmt#2698.92.0:2730.92.32"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.mmt#3107.104.0:3230.104.123"/></metadata>all other fields of both action and representation are deduced from the group and the set, so i guess this is enough?</opaque><mref name="[http://mathhub.info/MitM/groups?group_action_is_permutation_representation]" target="http://mathhub.info/MitM/groups?group_action_is_permutation_representation"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.mmt#3232.105.0:3278.105.46"/></metadata></mref><mref name="[http://mathhub.info/MitM/groups?permutation_representation_is_group_action]" target="http://mathhub.info/MitM/groups?permutation_representation_is_group_action"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.mmt#3425.110.0:3471.110.46"/></metadata></mref><mref name="[http://mathhub.info/MitM/groups?group_action_stabilizer]" target="http://mathhub.info/MitM/groups?group_action_stabilizer"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.mmt#4011.127.0:4040.127.29"/></metadata></mref><mref name="[http://mathhub.info/MitM/groups?orbit_stabilizer_theorem]" target="http://mathhub.info/MitM/groups?orbit_stabilizer_theorem"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.mmt#4368.138.0:4398.138.30"/></metadata></mref><mref name="[http://mathhub.info/MitM/groups?conjugation]" target="http://mathhub.info/MitM/groups?conjugation"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.mmt#4921.158.0:4936.158.15"/></metadata></mref><mref name="[http://mathhub.info/MitM/groups?conjugation_centralizer]" target="http://mathhub.info/MitM/groups?conjugation_centralizer"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.mmt#4993.163.0:5022.163.29"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/algebra/lattice.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#0.0.0:4939.144.0"/></metadata><mref name="[http://mathhub.info/MitM/smglom/algebra?IdempotentMagma]" target="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#157.4.0:178.4.21"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?Band]" target="http://mathhub.info/MitM/smglom/algebra?Band"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#418.14.0:428.14.10"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?SemiLattice]" target="http://mathhub.info/MitM/smglom/algebra?SemiLattice"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#659.23.0:676.23.17"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#1840.57.0:2298.67.0"/></metadata>MiKo: probably need to say that the meet order is the same as the join-order, i.e.
<omdoc base="http://mathhub.info/MitM/smglom/algebra/lattice.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#0.0.0:4463.125.0"/></metadata><mref name="[http://mathhub.info/MitM/smglom/algebra?SemiLattice]" target="http://mathhub.info/MitM/smglom/algebra?SemiLattice"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#157.4.0:174.4.17"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#1364.38.0:1822.48.0"/></metadata>MiKo: probably need to say that the meet order is the same as the join-order, i.e.
in theory SemiLattice/semilattice_theory
biviewMeet : ⊢ SemilatticeIsPOSet (POSetIsMeetSemiLattice op ) ≐ op
biviewJoin : ⊢ SemilatticeIsPOSet (POSetIsJoinSemiLattice op ) ≐ op
......@@ -8,4 +8,4 @@ in theory SemiLattice/semilattice_theory
theory ts:?POSet/poset_theory
biviewMeet : ⊢ POSetIsMeetSemiLattice (SemilatticeIsPOSet ord ) ≐ ord
biviewMeet : ⊢ POSetIsMeetSemiLattice (SemilatticeIsPOSet ord ) ≐ ord</opaque><mref name="[http://mathhub.info/MitM/smglom/algebra?Lattice]" target="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#2301.69.0:2314.69.13"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?DistributiveLattice]" target="http://mathhub.info/MitM/smglom/algebra?DistributiveLattice"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3425.99.0:3450.99.25"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?BoundedLattice]" target="http://mathhub.info/MitM/smglom/algebra?BoundedLattice"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3797.113.0:3817.113.20"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?ComplementedLattice]" target="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#4180.126.0:4205.126.25"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra]" target="http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#4624.137.0:4644.137.20"/></metadata></mref></omdoc>
\ No newline at end of file
biviewMeet : ⊢ POSetIsMeetSemiLattice (SemilatticeIsPOSet ord ) ≐ ord</opaque><mref name="[http://mathhub.info/MitM/smglom/algebra?Lattice]" target="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#1825.50.0:1838.50.13"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?DistributiveLattice]" target="http://mathhub.info/MitM/smglom/algebra?DistributiveLattice"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#2949.80.0:2974.80.25"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?BoundedLattice]" target="http://mathhub.info/MitM/smglom/algebra?BoundedLattice"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#3321.94.0:3341.94.20"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?ComplementedLattice]" target="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#3704.107.0:3729.107.25"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra]" target="http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/lattice.mmt#4148.118.0:4168.118.20"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/elliptic_curves/algebra_base.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/elliptic_curves/algebra_base.mmt#0.0.0:579.15.0"/></metadata><mref name="[http://mathhub.info/MitM/smglom/elliptic_curves?Base]" target="http://mathhub.info/MitM/smglom/elliptic_curves?Base"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/elliptic_curves/algebra_base.mmt#169.5.0:179.5.10"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://mathhub.info/MitM/smglom/elliptic_curves/algebra_base.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/elliptic_curves/algebra_base.mmt#0.0.0:580.15.0"/></metadata><mref name="[http://mathhub.info/MitM/smglom/elliptic_curves?Base]" target="http://mathhub.info/MitM/smglom/elliptic_curves?Base"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/elliptic_curves/algebra_base.mmt#169.5.0:179.5.10"/></metadata></mref></omdoc>
\ No newline at end of file
document http://mathhub.info/MitM/smglom/algebra/bands.omdoc
Declares http://mathhub.info/MitM/smglom/algebra/bands.omdoc http://mathhub.info/MitM/smglom/algebra?IdempotentMagma
Declares http://mathhub.info/MitM/smglom/algebra/bands.omdoc http://mathhub.info/MitM/smglom/algebra/bands?Band
Declares http://mathhub.info/MitM/smglom/algebra/bands.omdoc http://mathhub.info/MitM/smglom/algebra/bands?Regular
Declares http://mathhub.info/MitM/smglom/algebra/bands.omdoc http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal
Declares http://mathhub.info/MitM/smglom/algebra/bands.omdoc http://mathhub.info/MitM/smglom/algebra/bands?RightNormal
Declares http://mathhub.info/MitM/smglom/algebra/bands.omdoc http://mathhub.info/MitM/smglom/algebra/bands?Normal
document http://mathhub.info/MitM/smglom/algebra/computational_groups
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups http://mathhub.info/MitM/smglom/algebra/computational_groups/ActingOnPolynomials.omdoc
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups http://mathhub.info/MitM/smglom/algebra/computational_groups/GroupActions.omdoc
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups http://mathhub.info/MitM/smglom/algebra/computational_groups/Groups.omdoc
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups http://mathhub.info/MitM/smglom/algebra/computational_groups/PermutationGroups.omdoc
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups http://mathhub.info/MitM/smglom/algebra/computational_groups/StabilizerChain.omdoc
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups http://mathhub.info/MitM/smglom/algebra/computational_groups/SymmetricGroups.omdoc
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.omdoc
document http://mathhub.info/MitM/smglom/algebra/computational_groups/ActingOnPolynomials.omdoc
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups/ActingOnPolynomials.omdoc http://mathhub.info/MitM/smglom/algebra/computational_groups/ActingOnPolynomials.omdoc/opaque_909423254
document http://mathhub.info/MitM/smglom/algebra/computational_groups/GroupActions.omdoc
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups/GroupActions.omdoc http://mathhub.info/MitM/smglom/algebra/groups?GroupActions
document http://mathhub.info/MitM/smglom/algebra/computational_groups/Groups.omdoc
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups/Groups.omdoc http://mathhub.info/MitM/smglom/algebra/groups?Subgroups
document http://mathhub.info/MitM/smglom/algebra/computational_groups/PermutationGroups.omdoc
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups/PermutationGroups.omdoc http://mathhub.info/MitM/smglom/algebra/computational_groups/PermutationGroups.omdoc/opaque_1461772012
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups/PermutationGroups.omdoc http://mathhub.info/MitM/smglom/algebra/groups?PermutationGroups
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups/PermutationGroups.omdoc http://mathhub.info/MitM/smglom/algebra/groups?PermutationGroupsN
document http://mathhub.info/MitM/smglom/algebra/computational_groups/StabilizerChain.omdoc
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups/StabilizerChain.omdoc http://mathhub.info/MitM/smglom/algebra/groups?StabilizerChain
document http://mathhub.info/MitM/smglom/algebra/computational_groups/SymmetricGroups.omdoc
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups/SymmetricGroups.omdoc http://mathhub.info/MitM/smglom/algebra/groups?SymmetricGroup
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups/SymmetricGroups.omdoc http://mathhub.info/MitM/smglom/algebra/groups?SymmetricGroupOfN
document http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.omdoc
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.omdoc http://mathhub.info/MitM/groups?SylowSubgroup
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.omdoc http://mathhub.info/MitM/groups?left_coset
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.omdoc http://mathhub.info/MitM/groups?normal_subgroup
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.omdoc http://mathhub.info/MitM/groups?group_homomorphism
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.omdoc http://mathhub.info/MitM/groups?group_action
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.omdoc http://mathhub.info/MitM/groups?permutation_representation
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.omdoc http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.omdoc/opaque_1929379659
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.omdoc http://mathhub.info/MitM/groups?group_action_is_permutation_representation
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.omdoc http://mathhub.info/MitM/groups?permutation_representation_is_group_action
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.omdoc http://mathhub.info/MitM/groups?group_action_stabilizer
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.omdoc http://mathhub.info/MitM/groups?orbit_stabilizer_theorem
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.omdoc http://mathhub.info/MitM/groups?conjugation
Declares http://mathhub.info/MitM/smglom/algebra/computational_groups/abbatoir.omdoc http://mathhub.info/MitM/groups?conjugation_centralizer
document http://mathhub.info/MitM/smglom/algebra/lattice.omdoc
Declares http://mathhub.info/MitM/smglom/algebra/lattice.omdoc http://mathhub.info/MitM/smglom/algebra?IdempotentMagma
Declares http://mathhub.info/MitM/smglom/algebra/lattice.omdoc http://mathhub.info/MitM/smglom/algebra?Band
Declares http://mathhub.info/MitM/smglom/algebra/lattice.omdoc http://mathhub.info/MitM/smglom/algebra?SemiLattice
Declares http://mathhub.info/MitM/smglom/algebra/lattice.omdoc http://mathhub.info/MitM/smglom/algebra/lattice.omdoc/opaque_728804595
Declares http://mathhub.info/MitM/smglom/algebra/lattice.omdoc http://mathhub.info/MitM/smglom/algebra?Lattice
......
dataconstructor http://mathhub.info/MitM/groups?SylowSubgroup?FromTheory
dataconstructor http://mathhub.info/MitM/groups?SylowSubgroup?is_right_coset
theory http://mathhub.info/MitM/groups?SylowSubgroup
HasMeta http://mathhub.info/MitM/groups?SylowSubgroup http://mathhub.info/MitM/Foundation?Logic
Declares http://mathhub.info/MitM/groups?SylowSubgroup http://mathhub.info/MitM/groups?SylowSubgroup?right_coset
theory http://mathhub.info/MitM/groups?SylowSubgroup/right_coset
HasMeta http://mathhub.info/MitM/groups?SylowSubgroup/right_coset http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/groups?SylowSubgroup/right_coset http://mathhub.info/MitM/groups?subgroup
Declares http://mathhub.info/MitM/groups?SylowSubgroup/right_coset http://mathhub.info/MitM/groups?SylowSubgroup/right_coset?right_coset_theory
theory http://mathhub.info/MitM/groups?SylowSubgroup/right_coset/right_coset_theory
HasMeta http://mathhub.info/MitM/groups?SylowSubgroup/right_coset/right_coset_theory http://mathhub.info/MitM/Foundation?Logic
Declares http://mathhub.info/MitM/groups?SylowSubgroup/right_coset http://mathhub.info/MitM/groups?SylowSubgroup/right_coset?type_of_coset
constant http://mathhub.info/MitM/groups?SylowSubgroup/right_coset?type_of_coset
Declares http://mathhub.info/MitM/groups?SylowSubgroup http://mathhub.info/MitM/groups?SylowSubgroup?FromTheory
constant http://mathhub.info/MitM/groups?SylowSubgroup?FromTheory
Declares http://mathhub.info/MitM/groups?SylowSubgroup http://mathhub.info/MitM/groups?SylowSubgroup?is_right_coset
constant http://mathhub.info/MitM/groups?SylowSubgroup?is_right_coset
dataconstructor http://mathhub.info/MitM/groups?conjugation?G
dataconstructor http://mathhub.info/MitM/groups?conjugation?Ω
dataconstructor http://mathhub.info/MitM/groups?conjugation?la
dataconstructor http://mathhub.info/MitM/groups?conjugation?ra
dataconstructor http://mathhub.info/MitM/groups?conjugation?conjugation
theory http://mathhub.info/MitM/groups?conjugation
HasMeta http://mathhub.info/MitM/groups?conjugation http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/groups?conjugation http://mathhub.info/MitM/groups?group
Includes http://mathhub.info/MitM/groups?conjugation http://mathhub.info/MitM/groups?group_action
Declares http://mathhub.info/MitM/groups?conjugation http://mathhub.info/MitM/groups?conjugation?G
constant http://mathhub.info/MitM/groups?conjugation?G
Declares http://mathhub.info/MitM/groups?conjugation http://mathhub.info/MitM/groups?conjugation?Ω
constant http://mathhub.info/MitM/groups?conjugation?Ω
Declares http://mathhub.info/MitM/groups?conjugation http://mathhub.info/MitM/groups?conjugation?la
constant http://mathhub.info/MitM/groups?conjugation?la
Declares http://mathhub.info/MitM/groups?conjugation http://mathhub.info/MitM/groups?conjugation?ra
constant http://mathhub.info/MitM/groups?conjugation?ra
Declares http://mathhub.info/MitM/groups?conjugation http://mathhub.info/MitM/groups?conjugation?conjugation
constant http://mathhub.info/MitM/groups?conjugation?conjugation
dataconstructor http://mathhub.info/MitM/groups?conjugation_centralizer?centralizer
theory http://mathhub.info/MitM/groups?conjugation_centralizer
HasMeta http://mathhub.info/MitM/groups?conjugation_centralizer http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/groups?conjugation_centralizer http://mathhub.info/MitM/groups?conjugation
Includes http://mathhub.info/MitM/groups?conjugation_centralizer http://mathhub.info/MitM/groups?group_action_stabilizer
Declares http://mathhub.info/MitM/groups?conjugation_centralizer http://mathhub.info/MitM/groups?conjugation_centralizer?centralizer
constant http://mathhub.info/MitM/groups?conjugation_centralizer?centralizer
dataconstructor http://mathhub.info/MitM/groups?group_action?actee
dataconstructor http://mathhub.info/MitM/groups?group_action?map
dataconstructor http://mathhub.info/MitM/groups?group_action?right_group_action_property_id
dataconstructor http://mathhub.info/MitM/groups?group_action?right_group_action_property_prod
theory http://mathhub.info/MitM/groups?group_action
HasMeta http://mathhub.info/MitM/groups?group_action http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/groups?group_action http://mathhub.info/MitM/groups?group
Declares http://mathhub.info/MitM/groups?group_action http://mathhub.info/MitM/groups?group_action?right_group_action_theory
theory http://mathhub.info/MitM/groups?group_action/right_group_action_theory
HasMeta http://mathhub.info/MitM/groups?group_action/right_group_action_theory http://mathhub.info/MitM/Foundation?Logic
Declares http://mathhub.info/MitM/groups?group_action http://mathhub.info/MitM/groups?group_action?actee
constant http://mathhub.info/MitM/groups?group_action?actee
Declares http://mathhub.info/MitM/groups?group_action http://mathhub.info/MitM/groups?group_action?map
constant http://mathhub.info/MitM/groups?group_action?map
Declares http://mathhub.info/MitM/groups?group_action http://mathhub.info/MitM/groups?group_action?right_group_action_property_id
constant http://mathhub.info/MitM/groups?group_action?right_group_action_property_id
Declares http://mathhub.info/MitM/groups?group_action http://mathhub.info/MitM/groups?group_action?right_group_action_property_prod
constant http://mathhub.info/MitM/groups?group_action?right_group_action_property_prod
HasDomain http://mathhub.info/MitM/groups?group_action_is_permutation_representation http://mathhub.info/MitM/groups?group_action/rightgroupaction
HasCodomain http://mathhub.info/MitM/groups?group_action_is_permutation_representation http://mathhub.info/MitM/groups?permutation_representation/permutation_representation
view http://mathhub.info/MitM/groups?group_action_is_permutation_representation
HasViewFrom http://mathhub.info/MitM/groups?permutation_representation/permutation_representation http://mathhub.info/MitM/groups?group_action/rightgroupaction
dataconstructor http://mathhub.info/MitM/groups?group_action_stabilizer?element
dataconstructor http://mathhub.info/MitM/groups?group_action_stabilizer?stabilizer
dataconstructor http://mathhub.info/MitM/groups?group_action_stabilizer?stabilizer_set_binding
dataconstructor http://mathhub.info/MitM/groups?group_action_stabilizer?order
theory http://mathhub.info/MitM/groups?group_action_stabilizer
HasMeta http://mathhub.info/MitM/groups?group_action_stabilizer http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/groups?group_action_stabilizer http://mathhub.info/MitM/groups?group_action
Declares http://mathhub.info/MitM/groups?group_action_stabilizer http://mathhub.info/MitM/groups?group_action_stabilizer?stabilizer_theory
theory http://mathhub.info/MitM/groups?group_action_stabilizer/stabilizer_theory
HasMeta http://mathhub.info/MitM/groups?group_action_stabilizer/stabilizer_theory http://mathhub.info/MitM/Foundation?Logic
Declares http://mathhub.info/MitM/groups?group_action_stabilizer http://mathhub.info/MitM/groups?group_action_stabilizer?element
constant http://mathhub.info/MitM/groups?group_action_stabilizer?element
Declares http://mathhub.info/MitM/groups?group_action_stabilizer http://mathhub.info/MitM/groups?group_action_stabilizer?stabilizer
constant http://mathhub.info/MitM/groups?group_action_stabilizer?stabilizer
Declares http://mathhub.info/MitM/groups?group_action_stabilizer http://mathhub.info/MitM/groups?group_action_stabilizer?stabilizer_set_binding
constant http://mathhub.info/MitM/groups?group_action_stabilizer?stabilizer_set_binding
Declares http://mathhub.info/MitM/groups?group_action_stabilizer http://mathhub.info/MitM/groups?group_action_stabilizer?order
constant http://mathhub.info/MitM/groups?group_action_stabilizer?order
dataconstructor http://mathhub.info/MitM/groups?group_homomorphism?to
dataconstructor http://mathhub.info/MitM/groups?group_homomorphism?map
dataconstructor http://mathhub.info/MitM/groups?group_homomorphism?morphism_property
theory http://mathhub.info/MitM/groups?group_homomorphism
HasMeta http://mathhub.info/MitM/groups?group_homomorphism http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/groups?group_homomorphism http://mathhub.info/MitM/groups?group
Declares http://mathhub.info/MitM/groups?group_homomorphism http://mathhub.info/MitM/groups?group_homomorphism?group_homomorphism_theory
theory http://mathhub.info/MitM/groups?group_homomorphism/group_homomorphism_theory
HasMeta http://mathhub.info/MitM/groups?group_homomorphism/group_homomorphism_theory http://mathhub.info/MitM/Foundation?Logic
Declares http://mathhub.info/MitM/groups?group_homomorphism http://mathhub.info/MitM/groups?group_homomorphism?to
constant http://mathhub.info/MitM/groups?group_homomorphism?to
Declares http://mathhub.info/MitM/groups?group_homomorphism http://mathhub.info/MitM/groups?group_homomorphism?map
constant http://mathhub.info/MitM/groups?group_homomorphism?map
Declares http://mathhub.info/MitM/groups?group_homomorphism http://mathhub.info/MitM/groups?group_homomorphism?morphism_property
constant http://mathhub.info/MitM/groups?group_homomorphism?morphism_property
dataconstructor http://mathhub.info/MitM/groups?left_coset?left_coset
theory http://mathhub.info/MitM/groups?left_coset
HasMeta http://mathhub.info/MitM/groups?left_coset http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/groups?left_coset http://mathhub.info/MitM/groups?subgroup
Declares http://mathhub.info/MitM/groups?left_coset http://mathhub.info/MitM/groups?left_coset?left_coset_theory
theory http://mathhub.info/MitM/groups?left_coset/left_coset_theory
HasMeta http://mathhub.info/MitM/groups?left_coset/left_coset_theory http://mathhub.info/MitM/Foundation?Logic
Declares http://mathhub.info/MitM/groups?left_coset http://mathhub.info/MitM/groups?left_coset?left_coset
constant http://mathhub.info/MitM/groups?left_coset?left_coset
dataconstructor http://mathhub.info/MitM/groups?normal_subgroup?is_normal_subgroup
theory http://mathhub.info/MitM/groups?normal_subgroup
HasMeta http://mathhub.info/MitM/groups?normal_subgroup http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/groups?normal_subgroup http://mathhub.info/MitM/groups?subgroup
Includes http://mathhub.info/MitM/groups?normal_subgroup http://mathhub.info/MitM/groups?left_coset
Includes http://mathhub.info/MitM/groups?normal_subgroup http://mathhub.info/MitM/groups?right_coset
Includes http://mathhub.info/MitM/groups?normal_subgroup http://mathhub.info/MitM/groups?set_equality
Declares http://mathhub.info/MitM/groups?normal_subgroup http://mathhub.info/MitM/groups?normal_subgroup?is_normal_subgroup
constant http://mathhub.info/MitM/groups?normal_subgroup?is_normal_subgroup
dataconstructor http://mathhub.info/MitM/groups?orbit_stabilizer_theorem?Omega
dataconstructor http://mathhub.info/MitM/groups?orbit_stabilizer_theorem?G
dataconstructor http://mathhub.info/MitM/groups?orbit_stabilizer_theorem?action
dataconstructor http://mathhub.info/MitM/groups?orbit_stabilizer_theorem?theorem
theory http://mathhub.info/MitM/groups?orbit_stabilizer_theorem
HasMeta http://mathhub.info/MitM/groups?orbit_stabilizer_theorem http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/groups?orbit_stabilizer_theorem http://mathhub.info/MitM/groups?group_action
Includes http://mathhub.info/MitM/groups?orbit_stabilizer_theorem http://mathhub.info/MitM/groups?group_action_orbit
Includes http://mathhub.info/MitM/groups?orbit_stabilizer_theorem http://mathhub.info/MitM/groups?group_action_stabilizer
Declares http://mathhub.info/MitM/groups?orbit_stabilizer_theorem http://mathhub.info/MitM/groups?orbit_stabilizer_theorem?Omega
constant http://mathhub.info/MitM/groups?orbit_stabilizer_theorem?Omega
Declares http://mathhub.info/MitM/groups?orbit_stabilizer_theorem http://mathhub.info/MitM/groups?orbit_stabilizer_theorem?G
constant http://mathhub.info/MitM/groups?orbit_stabilizer_theorem?G
Declares http://mathhub.info/MitM/groups?orbit_stabilizer_theorem http://mathhub.info/MitM/groups?orbit_stabilizer_theorem?action
constant http://mathhub.info/MitM/groups?orbit_stabilizer_theorem?action
Declares http://mathhub.info/MitM/groups?orbit_stabilizer_theorem http://mathhub.info/MitM/groups?orbit_stabilizer_theorem?theorem
constant http://mathhub.info/MitM/groups?orbit_stabilizer_theorem?theorem
dataconstructor http://mathhub.info/MitM/groups?permutation_representation?actee_set
dataconstructor http://mathhub.info/MitM/groups?permutation_representation?hom
theory http://mathhub.info/MitM/groups?permutation_representation
HasMeta http://mathhub.info/MitM/groups?permutation_representation http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/groups?permutation_representation http://mathhub.info/MitM/groups?group
Includes http://mathhub.info/MitM/groups?permutation_representation http://mathhub.info/MitM/groups?group_homomorphism
Includes http://mathhub.info/MitM/groups?permutation_representation http://mathhub.info/MitM/groups?SymmetricGroup
Declares http://mathhub.info/MitM/groups?permutation_representation http://mathhub.info/MitM/groups?permutation_representation?permutation_representation_theory
theory http://mathhub.info/MitM/groups?permutation_representation/permutation_representation_theory
HasMeta http://mathhub.info/MitM/groups?permutation_representation/permutation_representation_theory http://mathhub.info/MitM/Foundation?Logic
Declares http://mathhub.info/MitM/groups?permutation_representation http://mathhub.info/MitM/groups?permutation_representation?actee_set
constant http://mathhub.info/MitM/groups?permutation_representation?actee_set
Declares http://mathhub.info/MitM/groups?permutation_representation http://mathhub.info/MitM/groups?permutation_representation?hom
constant http://mathhub.info/MitM/groups?permutation_representation?hom
HasDomain http://mathhub.info/MitM/groups?permutation_representation_is_group_action http://mathhub.info/MitM/groups?permutation_representation/permutation_representation
HasCodomain http://mathhub.info/MitM/groups?permutation_representation_is_group_action http://mathhub.info/MitM/groups?group_action/rightgroupaction
view http://mathhub.info/MitM/groups?permutation_representation_is_group_action
HasViewFrom http://mathhub.info/MitM/groups?group_action/rightgroupaction http://mathhub.info/MitM/groups?permutation_representation/permutation_representation
Declares http://mathhub.info/MitM/groups?permutation_representation_is_group_action http://mathhub.info/MitM/groups?permutation_representation_is_group_action?group_action_orbit
theory http://mathhub.info/MitM/groups?permutation_representation_is_group_action/group_action_orbit
HasMeta http://mathhub.info/MitM/groups?permutation_representation_is_group_action/group_action_orbit http://mathhub.info/MitM/Foundation?Logic
Declares http://mathhub.info/MitM/groups?permutation_representation_is_group_action http://mathhub.info/MitM/groups?permutation_representation_is_group_action?orbit_theory
theory http://mathhub.info/MitM/groups?permutation_representation_is_group_action/orbit_theory
HasMeta http://mathhub.info/MitM/groups?permutation_representation_is_group_action/orbit_theory http://mathhub.info/MitM/Foundation?Logic
......@@ -29,7 +29,7 @@ Includes http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra http://gl.mathhu
Includes http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra http://mathhub.info/MitM/Foundation?ProductType
Includes http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra http://mathhub.info/MitM/smglom/typedsets?Relations
Includes http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra http://mathhub.info/MitM/smglom/algebra?IdempotentMagma
Includes http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra http://mathhub.info/MitM/smglom/algebra?Band
Includes http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra http://mathhub.info/MitM/smglom/algebra/bands?Band
Includes http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra http://mathhub.info/MitM/smglom/algebra?SemiLattice
Includes http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra http://mathhub.info/MitM/Foundation?NaturalDeduction
Includes http://mathhub.info/MitM/smglom/algebra?BooleanAlgebra http://mathhub.info/MitM/smglom/typedsets?FiniteCardinality
......
......@@ -29,7 +29,7 @@ Includes http://mathhub.info/MitM/smglom/algebra?BoundedLattice http://gl.mathhu
Includes http://mathhub.info/MitM/smglom/algebra?BoundedLattice http://mathhub.info/MitM/Foundation?ProductType
Includes http://mathhub.info/MitM/smglom/algebra?BoundedLattice http://mathhub.info/MitM/smglom/typedsets?Relations
Includes http://mathhub.info/MitM/smglom/algebra?BoundedLattice http://mathhub.info/MitM/smglom/algebra?IdempotentMagma
Includes http://mathhub.info/MitM/smglom/algebra?BoundedLattice http://mathhub.info/MitM/smglom/algebra?Band
Includes http://mathhub.info/MitM/smglom/algebra?BoundedLattice http://mathhub.info/MitM/smglom/algebra/bands?Band
Includes http://mathhub.info/MitM/smglom/algebra?BoundedLattice http://mathhub.info/MitM/smglom/algebra?SemiLattice
Includes http://mathhub.info/MitM/smglom/algebra?BoundedLattice http://mathhub.info/MitM/Foundation?NaturalDeduction
Includes http://mathhub.info/MitM/smglom/algebra?BoundedLattice http://mathhub.info/MitM/smglom/typedsets?FiniteCardinality
......
......@@ -29,7 +29,7 @@ Includes http://mathhub.info/MitM/smglom/algebra?ComplementedLattice http://gl.m
Includes http://mathhub.info/MitM/smglom/algebra?ComplementedLattice http://mathhub.info/MitM/Foundation?ProductType
Includes http://mathhub.info/MitM/smglom/algebra?ComplementedLattice http://mathhub.info/MitM/smglom/typedsets?Relations
Includes http://mathhub.info/MitM/smglom/algebra?ComplementedLattice http://mathhub.info/MitM/smglom/algebra?IdempotentMagma
Includes http://mathhub.info/MitM/smglom/algebra?ComplementedLattice http://mathhub.info/MitM/smglom/algebra?Band
Includes http://mathhub.info/MitM/smglom/algebra?ComplementedLattice http://mathhub.info/MitM/smglom/algebra/bands?Band
Includes http://mathhub.info/MitM/smglom/algebra?ComplementedLattice http://mathhub.info/MitM/smglom/algebra?SemiLattice
Includes http://mathhub.info/MitM/smglom/algebra?ComplementedLattice http://mathhub.info/MitM/Foundation?NaturalDeduction
Includes http://mathhub.info/MitM/smglom/algebra?ComplementedLattice http://mathhub.info/MitM/smglom/typedsets?FiniteCardinality
......
......@@ -29,7 +29,7 @@ Includes http://mathhub.info/MitM/smglom/algebra?DistributiveLattice http://gl.m
Includes http://mathhub.info/MitM/smglom/algebra?DistributiveLattice http://mathhub.info/MitM/Foundation?ProductType
Includes http://mathhub.info/MitM/smglom/algebra?DistributiveLattice http://mathhub.info/MitM/smglom/typedsets?Relations
Includes http://mathhub.info/MitM/smglom/algebra?DistributiveLattice http://mathhub.info/MitM/smglom/algebra?IdempotentMagma
Includes http://mathhub.info/MitM/smglom/algebra?DistributiveLattice http://mathhub.info/MitM/smglom/algebra?Band
Includes http://mathhub.info/MitM/smglom/algebra?DistributiveLattice http://mathhub.info/MitM/smglom/algebra/bands?Band
Includes http://mathhub.info/MitM/smglom/algebra?DistributiveLattice http://mathhub.info/MitM/smglom/algebra?SemiLattice
Includes http://mathhub.info/MitM/smglom/algebra?DistributiveLattice http://mathhub.info/MitM/Foundation?NaturalDeduction
Includes http://mathhub.info/MitM/smglom/algebra?DistributiveLattice http://mathhub.info/MitM/smglom/typedsets?FiniteCardinality
......
......@@ -2,6 +2,8 @@ highuniverse http://mathhub.info/MitM/smglom/algebra?IdempotentMagma?idempotentM
theory http://mathhub.info/MitM/smglom/algebra?IdempotentMagma
HasMeta http://mathhub.info/MitM/smglom/algebra?IdempotentMagma http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/smglom/algebra?IdempotentMagma http://mathhub.info/MitM/smglom/algebra?OperationProps
Includes http://mathhub.info/MitM/smglom/algebra?IdempotentMagma http://mathhub.info/MitM/Foundation?Strings
Includes http://mathhub.info/MitM/smglom/algebra?IdempotentMagma http://mathhub.info/MitM/Foundation?InformalProofs
Declares http://mathhub.info/MitM/smglom/algebra?IdempotentMagma http://mathhub.info/MitM/smglom/algebra?IdempotentMagma?idempotent_theory
theory http://mathhub.info/MitM/smglom/algebra?IdempotentMagma/idempotent_theory
HasMeta http://mathhub.info/MitM/smglom/algebra?IdempotentMagma/idempotent_theory http://mathhub.info/MitM/Foundation?Logic
......
......@@ -29,7 +29,7 @@ Includes http://mathhub.info/MitM/smglom/algebra?Lattice http://gl.mathhub.info/
Includes http://mathhub.info/MitM/smglom/algebra?Lattice http://mathhub.info/MitM/Foundation?ProductType
Includes http://mathhub.info/MitM/smglom/algebra?Lattice http://mathhub.info/MitM/smglom/typedsets?Relations
Includes http://mathhub.info/MitM/smglom/algebra?Lattice http://mathhub.info/MitM/smglom/algebra?IdempotentMagma
Includes http://mathhub.info/MitM/smglom/algebra?Lattice http://mathhub.info/MitM/smglom/algebra?Band
Includes http://mathhub.info/MitM/smglom/algebra?Lattice http://mathhub.info/MitM/smglom/algebra/bands?Band
Includes http://mathhub.info/MitM/smglom/algebra?Lattice http://mathhub.info/MitM/smglom/algebra?SemiLattice
Includes http://mathhub.info/MitM/smglom/algebra?Lattice http://mathhub.info/MitM/Foundation?NaturalDeduction
Includes http://mathhub.info/MitM/smglom/algebra?Lattice http://mathhub.info/MitM/smglom/typedsets?FiniteCardinality
......@@ -92,10 +92,10 @@ HasCodomain http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?meets
structure http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?meetstruct/[http://mathhub.info/MitM/smglom/algebra?SemiGroup/semigroup_theory]
Declares http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?meetstruct/[http://mathhub.info/MitM/smglom/algebra?SemiGroup/semigroup_theory]/axiom_associative
constant http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?meetstruct/[http://mathhub.info/MitM/smglom/algebra?SemiGroup/semigroup_theory]/axiom_associative
Declares http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?meetstruct/[http://mathhub.info/MitM/smglom/algebra?Band/band_theory]
HasDomain http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?meetstruct/[http://mathhub.info/MitM/smglom/algebra?Band/band_theory] http://mathhub.info/MitM/smglom/algebra?Band/band_theory
HasCodomain http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?meetstruct/[http://mathhub.info/MitM/smglom/algebra?Band/band_theory] http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory
structure http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?meetstruct/[http://mathhub.info/MitM/smglom/algebra?Band/band_theory]
Declares http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?meetstruct/[http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory]
HasDomain http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?meetstruct/[http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory] http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory
HasCodomain http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?meetstruct/[http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory] http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory
structure http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?meetstruct/[http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory]
Declares http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?meetstruct/axiom_commutative
constant http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?meetstruct/axiom_commutative
Declares http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?joinstruct
......@@ -127,10 +127,10 @@ HasCodomain http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?joins
structure http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?joinstruct/[http://mathhub.info/MitM/smglom/algebra?SemiGroup/semigroup_theory]
Declares http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?joinstruct/[http://mathhub.info/MitM/smglom/algebra?SemiGroup/semigroup_theory]/axiom_associative
constant http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?joinstruct/[http://mathhub.info/MitM/smglom/algebra?SemiGroup/semigroup_theory]/axiom_associative
Declares http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?joinstruct/[http://mathhub.info/MitM/smglom/algebra?Band/band_theory]
HasDomain http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?joinstruct/[http://mathhub.info/MitM/smglom/algebra?Band/band_theory] http://mathhub.info/MitM/smglom/algebra?Band/band_theory
HasCodomain http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?joinstruct/[http://mathhub.info/MitM/smglom/algebra?Band/band_theory] http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory
structure http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?joinstruct/[http://mathhub.info/MitM/smglom/algebra?Band/band_theory]
Declares http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?joinstruct/[http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory]
HasDomain http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?joinstruct/[http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory] http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory
HasCodomain http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?joinstruct/[http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory] http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory
structure http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?joinstruct/[http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory]
Declares http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?joinstruct/axiom_commutative
constant http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?joinstruct/axiom_commutative
Declares http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory http://mathhub.info/MitM/smglom/algebra?Lattice/lattice_theory?prop_absorption1
......
......@@ -29,7 +29,7 @@ Includes http://mathhub.info/MitM/smglom/algebra?SemiLattice http://mathhub.info
Includes http://mathhub.info/MitM/smglom/algebra?SemiLattice http://mathhub.info/MitM/smglom/typedsets?Relations
Includes http://mathhub.info/MitM/smglom/algebra?SemiLattice http://mathhub.info/MitM/smglom/algebra?OperationProps
Includes http://mathhub.info/MitM/smglom/algebra?SemiLattice http://mathhub.info/MitM/smglom/algebra?IdempotentMagma
Includes http://mathhub.info/MitM/smglom/algebra?SemiLattice http://mathhub.info/MitM/smglom/algebra?Band
Includes http://mathhub.info/MitM/smglom/algebra?SemiLattice http://mathhub.info/MitM/smglom/algebra/bands?Band
Declares http://mathhub.info/MitM/smglom/algebra?SemiLattice http://mathhub.info/MitM/smglom/algebra?SemiLattice?semilattice_theory
theory http://mathhub.info/MitM/smglom/algebra?SemiLattice/semilattice_theory
HasMeta http://mathhub.info/MitM/smglom/algebra?SemiLattice/semilattice_theory http://mathhub.info/MitM/Foundation?Logic
......@@ -37,7 +37,7 @@ Includes http://mathhub.info/MitM/smglom/algebra?SemiLattice/semilattice_theory
Includes http://mathhub.info/MitM/smglom/algebra?SemiLattice/semilattice_theory http://mathhub.info/MitM/smglom/algebra?Magma/magma_theory
Includes http://mathhub.info/MitM/smglom/algebra?SemiLattice/semilattice_theory http://mathhub.info/MitM/smglom/algebra?IdempotentMagma/idempotent_theory
Includes http://mathhub.info/MitM/smglom/algebra?SemiLattice/semilattice_theory http://mathhub.info/MitM/smglom/algebra?SemiGroup/semigroup_theory
Includes http://mathhub.info/MitM/smglom/algebra?SemiLattice/semilattice_theory http://mathhub.info/MitM/smglom/algebra?Band/band_theory
Includes http://mathhub.info/MitM/smglom/algebra?SemiLattice/semilattice_theory http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory
Declares http://mathhub.info/MitM/smglom/algebra?SemiLattice/semilattice_theory http://mathhub.info/MitM/smglom/algebra?SemiLattice/semilattice_theory?axiom_commutative
constant http://mathhub.info/MitM/smglom/algebra?SemiLattice/semilattice_theory?axiom_commutative
Declares http://mathhub.info/MitM/smglom/algebra?SemiLattice http://mathhub.info/MitM/smglom/algebra?SemiLattice?semilattice
......
highuniverse http://mathhub.info/MitM/smglom/algebra/bands?Band?band
theory http://mathhub.info/MitM/smglom/algebra/bands?Band
HasMeta http://mathhub.info/MitM/smglom/algebra/bands?Band http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/smglom/algebra/bands?Band http://mathhub.info/MitM/smglom/algebra?OperationProps
Includes http://mathhub.info/MitM/smglom/algebra/bands?Band http://mathhub.info/MitM/Foundation?Strings
Includes http://mathhub.info/MitM/smglom/algebra/bands?Band http://mathhub.info/MitM/Foundation?InformalProofs
Includes http://mathhub.info/MitM/smglom/algebra/bands?Band http://mathhub.info/MitM/smglom/algebra?IdempotentMagma
Declares http://mathhub.info/MitM/smglom/algebra/bands?Band http://mathhub.info/MitM/smglom/algebra/bands?Band?band_theory
theory http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory
HasMeta http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory http://mathhub.info/MitM/smglom/typedsets?SetStructures/setstruct_theory
Includes http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory http://mathhub.info/MitM/smglom/algebra?Magma/magma_theory
Includes http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory http://mathhub.info/MitM/smglom/algebra?IdempotentMagma/idempotent_theory
Includes http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory http://mathhub.info/MitM/smglom/algebra?SemiGroup/semigroup_theory
Declares http://mathhub.info/MitM/smglom/algebra/bands?Band http://mathhub.info/MitM/smglom/algebra/bands?Band?band
constant http://mathhub.info/MitM/smglom/algebra/bands?Band?band
Declares http://mathhub.info/MitM/smglom/algebra/bands?Band http://mathhub.info/MitM/smglom/algebra/bands?Band?band/abbreviation
constant http://mathhub.info/MitM/smglom/algebra/bands?Band?band/abbreviation
theory http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal
HasMeta http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal http://mathhub.info/MitM/smglom/algebra?OperationProps
Includes http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal http://mathhub.info/MitM/Foundation?Strings
Includes http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal http://mathhub.info/MitM/Foundation?InformalProofs
Includes http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal http://mathhub.info/MitM/smglom/algebra?IdempotentMagma
Includes http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal http://mathhub.info/MitM/smglom/algebra/bands?Band
Includes http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal http://mathhub.info/MitM/smglom/algebra/bands?Regular
Declares http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal?leftnormal_theory
theory http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/leftnormal_theory
HasMeta http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/leftnormal_theory http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/leftnormal_theory http://mathhub.info/MitM/smglom/typedsets?SetStructures/setstruct_theory
Includes http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/leftnormal_theory http://mathhub.info/MitM/smglom/algebra?Magma/magma_theory
Includes http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/leftnormal_theory http://mathhub.info/MitM/smglom/algebra?IdempotentMagma/idempotent_theory
Includes http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/leftnormal_theory http://mathhub.info/MitM/smglom/algebra?SemiGroup/semigroup_theory
Includes http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/leftnormal_theory http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory
Declares http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/leftnormal_theory http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/leftnormal_theory?axiom_leftnormal
constant http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/leftnormal_theory?axiom_leftnormal
Declares http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal?Reg2LeftNormal
HasDomain http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal http://mathhub.info/MitM/smglom/algebra/bands?Regular/regular_theory
HasCodomain http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/leftnormal_theory
view http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal
HasViewFrom http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/leftnormal_theory http://mathhub.info/MitM/smglom/algebra/bands?Regular/regular_theory
Declares http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal?[http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory]
HasDomain http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal?[http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory] http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory
HasCodomain http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal?[http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory] http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal
structure http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal?[http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory]
Declares http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal?[http://mathhub.info/MitM/Foundation?Logic]
HasDomain http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal?[http://mathhub.info/MitM/Foundation?Logic] http://mathhub.info/MitM/Foundation?Logic
HasCodomain http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal?[http://mathhub.info/MitM/Foundation?Logic] http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal
structure http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal?[http://mathhub.info/MitM/Foundation?Logic]
Declares http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal?[http://mathhub.info/MitM/smglom/typedsets?SetStructures/setstruct_theory]
HasDomain http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal?[http://mathhub.info/MitM/smglom/typedsets?SetStructures/setstruct_theory] http://mathhub.info/MitM/smglom/typedsets?SetStructures/setstruct_theory
HasCodomain http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal?[http://mathhub.info/MitM/smglom/typedsets?SetStructures/setstruct_theory] http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal
structure http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal?[http://mathhub.info/MitM/smglom/typedsets?SetStructures/setstruct_theory]
Declares http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal?[http://mathhub.info/MitM/smglom/algebra?Magma/magma_theory]
HasDomain http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal?[http://mathhub.info/MitM/smglom/algebra?Magma/magma_theory] http://mathhub.info/MitM/smglom/algebra?Magma/magma_theory
HasCodomain http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal?[http://mathhub.info/MitM/smglom/algebra?Magma/magma_theory] http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal
structure http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal?[http://mathhub.info/MitM/smglom/algebra?Magma/magma_theory]
Declares http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal?[http://mathhub.info/MitM/smglom/algebra?IdempotentMagma/idempotent_theory]
HasDomain http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal?[http://mathhub.info/MitM/smglom/algebra?IdempotentMagma/idempotent_theory] http://mathhub.info/MitM/smglom/algebra?IdempotentMagma/idempotent_theory
HasCodomain http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal?[http://mathhub.info/MitM/smglom/algebra?IdempotentMagma/idempotent_theory] http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal
structure http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal?[http://mathhub.info/MitM/smglom/algebra?IdempotentMagma/idempotent_theory]
Declares http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal?[http://mathhub.info/MitM/smglom/algebra?SemiGroup/semigroup_theory]
HasDomain http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal?[http://mathhub.info/MitM/smglom/algebra?SemiGroup/semigroup_theory] http://mathhub.info/MitM/smglom/algebra?SemiGroup/semigroup_theory
HasCodomain http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal?[http://mathhub.info/MitM/smglom/algebra?SemiGroup/semigroup_theory] http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal
structure http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal?[http://mathhub.info/MitM/smglom/algebra?SemiGroup/semigroup_theory]
Declares http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal?[http://mathhub.info/MitM/smglom/algebra/bands?Regular/regular_theory]/axiom_regular
constant http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/Reg2LeftNormal?[http://mathhub.info/MitM/smglom/algebra/bands?Regular/regular_theory]/axiom_regular
IsImplicitly http://mathhub.info/MitM/smglom/algebra/bands?LeftNormal/leftnormal_theory http://mathhub.info/MitM/smglom/algebra/bands?Regular/regular_theory
theory http://mathhub.info/MitM/smglom/algebra/bands?Regular
HasMeta http://mathhub.info/MitM/smglom/algebra/bands?Regular http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/smglom/algebra/bands?Regular http://mathhub.info/MitM/smglom/algebra?OperationProps
Includes http://mathhub.info/MitM/smglom/algebra/bands?Regular http://mathhub.info/MitM/Foundation?Strings
Includes http://mathhub.info/MitM/smglom/algebra/bands?Regular http://mathhub.info/MitM/Foundation?InformalProofs
Includes http://mathhub.info/MitM/smglom/algebra/bands?Regular http://mathhub.info/MitM/smglom/algebra?IdempotentMagma
Includes http://mathhub.info/MitM/smglom/algebra/bands?Regular http://mathhub.info/MitM/smglom/algebra/bands?Band
Declares http://mathhub.info/MitM/smglom/algebra/bands?Regular http://mathhub.info/MitM/smglom/algebra/bands?Regular?regular_theory
theory http://mathhub.info/MitM/smglom/algebra/bands?Regular/regular_theory
HasMeta http://mathhub.info/MitM/smglom/algebra/bands?Regular/regular_theory http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/smglom/algebra/bands?Regular/regular_theory http://mathhub.info/MitM/smglom/typedsets?SetStructures/setstruct_theory
Includes http://mathhub.info/MitM/smglom/algebra/bands?Regular/regular_theory http://mathhub.info/MitM/smglom/algebra?Magma/magma_theory
Includes http://mathhub.info/MitM/smglom/algebra/bands?Regular/regular_theory http://mathhub.info/MitM/smglom/algebra?IdempotentMagma/idempotent_theory
Includes http://mathhub.info/MitM/smglom/algebra/bands?Regular/regular_theory http://mathhub.info/MitM/smglom/algebra?SemiGroup/semigroup_theory
Includes http://mathhub.info/MitM/smglom/algebra/bands?Regular/regular_theory http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory
Declares http://mathhub.info/MitM/smglom/algebra/bands?Regular/regular_theory http://mathhub.info/MitM/smglom/algebra/bands?Regular/regular_theory?axiom_regular
constant http://mathhub.info/MitM/smglom/algebra/bands?Regular/regular_theory?axiom_regular
theory http://mathhub.info/MitM/smglom/algebra/bands?RightNormal
HasMeta http://mathhub.info/MitM/smglom/algebra/bands?RightNormal http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/smglom/algebra/bands?RightNormal http://mathhub.info/MitM/smglom/algebra?OperationProps
Includes http://mathhub.info/MitM/smglom/algebra/bands?RightNormal http://mathhub.info/MitM/Foundation?Strings
Includes http://mathhub.info/MitM/smglom/algebra/bands?RightNormal http://mathhub.info/MitM/Foundation?InformalProofs
Includes http://mathhub.info/MitM/smglom/algebra/bands?RightNormal http://mathhub.info/MitM/smglom/algebra?IdempotentMagma
Includes http://mathhub.info/MitM/smglom/algebra/bands?RightNormal http://mathhub.info/MitM/smglom/algebra/bands?Band
Includes http://mathhub.info/MitM/smglom/algebra/bands?RightNormal http://mathhub.info/MitM/smglom/algebra/bands?Regular
Declares http://mathhub.info/MitM/smglom/algebra/bands?RightNormal http://mathhub.info/MitM/smglom/algebra/bands?RightNormal?rightnormal_theory
theory http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/rightnormal_theory
HasMeta http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/rightnormal_theory http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/rightnormal_theory http://mathhub.info/MitM/smglom/typedsets?SetStructures/setstruct_theory
Includes http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/rightnormal_theory http://mathhub.info/MitM/smglom/algebra?Magma/magma_theory
Includes http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/rightnormal_theory http://mathhub.info/MitM/smglom/algebra?IdempotentMagma/idempotent_theory
Includes http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/rightnormal_theory http://mathhub.info/MitM/smglom/algebra?SemiGroup/semigroup_theory
Includes http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/rightnormal_theory http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory
Declares http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/rightnormal_theory http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/rightnormal_theory?axiom_rightnormal
constant http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/rightnormal_theory?axiom_rightnormal
Declares http://mathhub.info/MitM/smglom/algebra/bands?RightNormal http://mathhub.info/MitM/smglom/algebra/bands?RightNormal?Reg2RightNormal
HasDomain http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal http://mathhub.info/MitM/smglom/algebra/bands?Regular/regular_theory
HasCodomain http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/rightnormal_theory
view http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal
HasViewFrom http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/rightnormal_theory http://mathhub.info/MitM/smglom/algebra/bands?Regular/regular_theory
Declares http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal?[http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory]
HasDomain http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal?[http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory] http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory
HasCodomain http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal?[http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory] http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal
structure http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal?[http://mathhub.info/MitM/smglom/algebra/bands?Band/band_theory]
Declares http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal?[http://mathhub.info/MitM/Foundation?Logic]
HasDomain http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal?[http://mathhub.info/MitM/Foundation?Logic] http://mathhub.info/MitM/Foundation?Logic
HasCodomain http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal?[http://mathhub.info/MitM/Foundation?Logic] http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal
structure http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal?[http://mathhub.info/MitM/Foundation?Logic]
Declares http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal?[http://mathhub.info/MitM/smglom/typedsets?SetStructures/setstruct_theory]
HasDomain http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal?[http://mathhub.info/MitM/smglom/typedsets?SetStructures/setstruct_theory] http://mathhub.info/MitM/smglom/typedsets?SetStructures/setstruct_theory
HasCodomain http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal?[http://mathhub.info/MitM/smglom/typedsets?SetStructures/setstruct_theory] http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal
structure http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal?[http://mathhub.info/MitM/smglom/typedsets?SetStructures/setstruct_theory]
Declares http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal?[http://mathhub.info/MitM/smglom/algebra?Magma/magma_theory]
HasDomain http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal?[http://mathhub.info/MitM/smglom/algebra?Magma/magma_theory] http://mathhub.info/MitM/smglom/algebra?Magma/magma_theory
HasCodomain http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal?[http://mathhub.info/MitM/smglom/algebra?Magma/magma_theory] http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal
structure http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal?[http://mathhub.info/MitM/smglom/algebra?Magma/magma_theory]
Declares http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal?[http://mathhub.info/MitM/smglom/algebra?IdempotentMagma/idempotent_theory]
HasDomain http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal?[http://mathhub.info/MitM/smglom/algebra?IdempotentMagma/idempotent_theory] http://mathhub.info/MitM/smglom/algebra?IdempotentMagma/idempotent_theory
HasCodomain http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal?[http://mathhub.info/MitM/smglom/algebra?IdempotentMagma/idempotent_theory] http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal
structure http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal?[http://mathhub.info/MitM/smglom/algebra?IdempotentMagma/idempotent_theory]
Declares http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal?[http://mathhub.info/MitM/smglom/algebra?SemiGroup/semigroup_theory]
HasDomain http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal?[http://mathhub.info/MitM/smglom/algebra?SemiGroup/semigroup_theory] http://mathhub.info/MitM/smglom/algebra?SemiGroup/semigroup_theory
HasCodomain http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal?[http://mathhub.info/MitM/smglom/algebra?SemiGroup/semigroup_theory] http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal
structure http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal?[http://mathhub.info/MitM/smglom/algebra?SemiGroup/semigroup_theory]
Declares http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal?[http://mathhub.info/MitM/smglom/algebra/bands?Regular/regular_theory]/axiom_regular
constant http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/Reg2RightNormal?[http://mathhub.info/MitM/smglom/algebra/bands?Regular/regular_theory]/axiom_regular
IsImplicitly http://mathhub.info/MitM/smglom/algebra/bands?RightNormal/rightnormal_theory http://mathhub.info/MitM/smglom/algebra/bands?Regular/regular_theory
dataconstructor http://mathhub.info/MitM/smglom/algebra/groups?GroupActions?act_property_id
dataconstructor http://mathhub.info/MitM/smglom/algebra/groups?GroupActions?act_property_compose
theory http://mathhub.info/MitM/smglom/algebra/groups?GroupActions
HasMeta http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://mathhub.info/MitM/smglom/algebra?OperationProps
Includes http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://mathhub.info/MitM/smglom/algebra?Magma
Includes http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://mathhub.info/MitM/smglom/algebra?SemiGroup
Includes http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://mathhub.info/MitM/smglom/algebra?Unital
Includes http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://mathhub.info/MitM/smglom/algebra?Monoid
Includes http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://mathhub.info/MitM/Foundation?OptionType
Includes http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://mathhub.info/MitM/Foundation?DescriptionOperator
Includes http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://mathhub.info/MitM/Foundation?NaturalDeduction
Includes http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://mathhub.info/MitM/smglom/algebra?Loop
Includes http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://gl.mathhub.info/MMT/LFX/Subtyping?SubSymbol
Includes http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://gl.mathhub.info/MMT/LFX/Subtyping?SubRules
Includes http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://gl.mathhub.info/MMT/LFX/Subtyping?JudgmentSymbol
Includes http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://gl.mathhub.info/MMT/LFX/Subtyping?JudgmentRules
Includes http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://gl.mathhub.info/MMT/LFX/Subtyping?PredSubSymbols
Includes http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://gl.mathhub.info/MMT/LFX/Subtyping?PredSubRules
Includes http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://gl.mathhub.info/MMT/LFX/Subtyping?AllSubtypes
Includes http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://gl.mathhub.info/MMT/LFX/Subtyping?PiRule
Includes http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://gl.mathhub.info/MMT/LFX/Subtyping?LFWithVariance
Includes http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://gl.mathhub.info/MMT/LFX/Subtyping?LFSubtyped
Includes http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://mathhub.info/MitM/Foundation?Subtyping
Includes http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://mathhub.info/MitM/Foundation?NatLiterals
Includes http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://mathhub.info/MitM/Foundation?IntLiterals
Includes http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://mathhub.info/MitM/Foundation?Strings
Includes http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://mathhub.info/MitM/Foundation?InformalProofs
Includes http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://mathhub.info/MitM/smglom/algebra?Group
Includes http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://mathhub.info/MitM/smglom/algebra/groups?Subgroups
Declares http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://mathhub.info/MitM/smglom/algebra/groups?GroupActions?RightGroupActionsTheory
theory http://mathhub.info/MitM/smglom/algebra/groups?GroupActions/RightGroupActionsTheory
HasMeta http://mathhub.info/MitM/smglom/algebra/groups?GroupActions/RightGroupActionsTheory http://mathhub.info/MitM/Foundation?Logic
Declares http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://mathhub.info/MitM/smglom/algebra/groups?GroupActions?act_property_id
constant http://mathhub.info/MitM/smglom/algebra/groups?GroupActions?act_property_id
Declares http://mathhub.info/MitM/smglom/algebra/groups?GroupActions http://mathhub.info/MitM/smglom/algebra/groups?GroupActions?act_property_compose
constant http://mathhub.info/MitM/smglom/algebra/groups?GroupActions?act_property_compose
dataconstructor http://mathhub.info/MitM/smglom/algebra/groups?PermutationGroupsN?permutationGroup
theory http://mathhub.info/MitM/smglom/algebra/groups?PermutationGroupsN
Includes http://mathhub.info/MitM/smglom/algebra/groups?PermutationGroupsN http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/smglom/algebra/groups?PermutationGroupsN http://mathhub.info/MitM/smglom/algebra?OperationProps
Includes http://mathhub.info/MitM/smglom/algebra/groups?PermutationGroupsN http://mathhub.info/MitM/smglom/algebra?Magma
Includes http://mathhub.info/MitM/smglom/algebra/groups?PermutationGroupsN http://mathhub.info/MitM/smglom/algebra?SemiGroup