Skip to content

Commit

Permalink
Deploying to gh-pages from @ 7069d03 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@andreasabel
andreasabel committed Sep 8, 2024
1 parent 47651e7 commit 6759e81
Show file tree
Hide file tree
Showing 240 changed files with 15,973 additions and 15,538 deletions.
28 changes: 14 additions & 14 deletions experimental/Algebra.Lattice.Properties.BooleanAlgebra.Expression.html
View file

Large diffs are not rendered by default.

57 changes: 38 additions & 19 deletions experimental/Algebra.Properties.CommutativeMagma.Divisibility.html
View file

Large diffs are not rendered by default.

6 changes: 3 additions & 3 deletions experimental/Algebra.Properties.CommutativeMonoid.Sum.html
View file

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion experimental/Algebra.Properties.CommutativeSemigroup.Divisibility.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@
<a id="954" class="Comment">-- Re-export the contents of divisibility over commutative magmas</a>

<a id="1021" class="Keyword">open</a> <a id="1026" class="Keyword">import</a> <a id="1033" href="Algebra.Properties.CommutativeMagma.Divisibility.html" class="Module">Algebra.Properties.CommutativeMagma.Divisibility</a> <a id="1082" href="Algebra.Bundles.html#5965" class="Function">commutativeMagma</a> <a id="1099" class="Keyword">public</a>
<a id="1108" class="Keyword">using</a> <a id="1114" class="Symbol">(</a><a id="1115" href="Algebra.Properties.CommutativeMagma.Divisibility.html#827" class="Function">x∣xy</a><a id="1119" class="Symbol">;</a> <a id="1121" href="Algebra.Properties.CommutativeMagma.Divisibility.html#877" class="Function">xy≈z⇒x∣z</a><a id="1129" class="Symbol">;</a> <a id="1131" href="Algebra.Properties.CommutativeMagma.Divisibility.html#963" class="Function">∣-factors</a><a id="1140" class="Symbol">;</a> <a id="1142" href="Algebra.Properties.CommutativeMagma.Divisibility.html#1046" class="Function">∣-factors-≈</a><a id="1153" class="Symbol">)</a>
<a id="1108" class="Keyword">using</a> <a id="1114" class="Symbol">(</a><a id="1115" href="Algebra.Properties.CommutativeMagma.Divisibility.html#800" class="Function">x∣xy</a><a id="1119" class="Symbol">;</a> <a id="1121" href="Algebra.Properties.CommutativeMagma.Divisibility.html#850" class="Function">xy≈z⇒x∣z</a><a id="1129" class="Symbol">;</a> <a id="1131" href="Algebra.Properties.CommutativeMagma.Divisibility.html#1409" class="Function">∣-factors</a><a id="1140" class="Symbol">;</a> <a id="1142" href="Algebra.Properties.CommutativeMagma.Divisibility.html#1542" class="Function">∣-factors-≈</a><a id="1153" class="Symbol">)</a>

<a id="1156" class="Comment">------------------------------------------------------------------------</a>
<a id="1229" class="Comment">-- New properties</a>
Expand Down
40 changes: 40 additions & 0 deletions experimental/Algebra.Properties.IdempotentCommutativeMonoid.html
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Algebra.Properties.IdempotentCommutativeMonoid</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">------------------------------------------------------------------------</a>
<a id="74" class="Comment">-- The Agda standard library</a>
<a id="103" class="Comment">--</a>
<a id="106" class="Comment">-- Some derivable properties</a>
<a id="135" class="Comment">------------------------------------------------------------------------</a>

<a id="209" class="Symbol">{-#</a> <a id="213" class="Keyword">OPTIONS</a> <a id="221" class="Pragma">--cubical-compatible</a> <a id="242" class="Pragma">--safe</a> <a id="249" class="Symbol">#-}</a>

<a id="254" class="Keyword">open</a> <a id="259" class="Keyword">import</a> <a id="266" href="Algebra.Bundles.html" class="Module">Algebra.Bundles</a> <a id="282" class="Keyword">using</a> <a id="288" class="Symbol">(</a><a id="289" href="Algebra.Bundles.html#9176" class="Record">IdempotentCommutativeMonoid</a><a id="316" class="Symbol">)</a>

<a id="319" class="Keyword">module</a> <a id="326" href="Algebra.Properties.IdempotentCommutativeMonoid.html" class="Module">Algebra.Properties.IdempotentCommutativeMonoid</a>
<a id="375" class="Symbol">{</a><a id="376" href="Algebra.Properties.IdempotentCommutativeMonoid.html#376" class="Bound">c</a> <a id="378" href="Algebra.Properties.IdempotentCommutativeMonoid.html#378" class="Bound">ℓ</a><a id="379" class="Symbol">}</a> <a id="381" class="Symbol">(</a><a id="382" href="Algebra.Properties.IdempotentCommutativeMonoid.html#382" class="Bound">M</a> <a id="384" class="Symbol">:</a> <a id="386" href="Algebra.Bundles.html#9176" class="Record">IdempotentCommutativeMonoid</a> <a id="414" href="Algebra.Properties.IdempotentCommutativeMonoid.html#376" class="Bound">c</a> <a id="416" href="Algebra.Properties.IdempotentCommutativeMonoid.html#378" class="Bound">ℓ</a><a id="417" class="Symbol">)</a> <a id="419" class="Keyword">where</a>

<a id="426" class="Keyword">open</a> <a id="431" href="Algebra.Bundles.html#9176" class="Module">IdempotentCommutativeMonoid</a> <a id="459" href="Algebra.Properties.IdempotentCommutativeMonoid.html#382" class="Bound">M</a>

<a id="462" class="Keyword">open</a> <a id="467" class="Keyword">import</a> <a id="474" href="Algebra.Consequences.Setoid.html" class="Module">Algebra.Consequences.Setoid</a> <a id="502" href="Algebra.Structures.html#1873" class="Function">setoid</a>
<a id="511" class="Keyword">using</a> <a id="517" class="Symbol">(</a><a id="518" href="Algebra.Consequences.Setoid.html#7938" class="Function">comm∧distrˡ⇒distrʳ</a><a id="536" class="Symbol">;</a> <a id="538" href="Algebra.Consequences.Setoid.html#8511" class="Function">comm∧distrˡ⇒distr</a><a id="555" class="Symbol">)</a>
<a id="557" class="Keyword">open</a> <a id="562" class="Keyword">import</a> <a id="569" href="Algebra.Definitions.html" class="Module">Algebra.Definitions</a> <a id="589" href="Algebra.Bundles.html#9318" class="Field Operator">_≈_</a>
<a id="595" class="Keyword">using</a> <a id="601" class="Symbol">(</a><a id="602" href="Algebra.Definitions.html#3220" class="Function Operator">_DistributesOverˡ_</a><a id="620" class="Symbol">;</a> <a id="622" href="Algebra.Definitions.html#3339" class="Function Operator">_DistributesOverʳ_</a><a id="640" class="Symbol">;</a> <a id="642" href="Algebra.Definitions.html#3458" class="Function Operator">_DistributesOver_</a><a id="659" class="Symbol">)</a>
<a id="661" class="Keyword">open</a> <a id="666" class="Keyword">import</a> <a id="673" href="Algebra.Properties.CommutativeSemigroup.html" class="Module">Algebra.Properties.CommutativeSemigroup</a> <a id="713" href="Algebra.Bundles.html#8392" class="Function">commutativeSemigroup</a>
<a id="736" class="Keyword">using</a> <a id="742" class="Symbol">(</a><a id="743" href="Algebra.Properties.CommutativeSemigroup.html#833" class="Function">interchange</a><a id="754" class="Symbol">)</a>
<a id="756" class="Keyword">open</a> <a id="761" class="Keyword">import</a> <a id="768" href="Relation.Binary.Reasoning.Setoid.html" class="Module">Relation.Binary.Reasoning.Setoid</a> <a id="801" href="Algebra.Structures.html#1873" class="Function">setoid</a>


<a id="810" class="Comment">------------------------------------------------------------------------</a>
<a id="883" class="Comment">-- Distributivity</a>

<a id="∙-distrˡ-∙"></a><a id="902" href="Algebra.Properties.IdempotentCommutativeMonoid.html#902" class="Function">∙-distrˡ-∙</a> <a id="913" class="Symbol">:</a> <a id="915" href="Algebra.Bundles.html#9368" class="Field Operator">_∙_</a> <a id="919" href="Algebra.Definitions.html#3220" class="Function Operator">DistributesOverˡ</a> <a id="936" href="Algebra.Bundles.html#9368" class="Field Operator">_∙_</a>
<a id="940" href="Algebra.Properties.IdempotentCommutativeMonoid.html#902" class="Function">∙-distrˡ-∙</a> <a id="951" href="Algebra.Properties.IdempotentCommutativeMonoid.html#951" class="Bound">a</a> <a id="953" href="Algebra.Properties.IdempotentCommutativeMonoid.html#953" class="Bound">b</a> <a id="955" href="Algebra.Properties.IdempotentCommutativeMonoid.html#955" class="Bound">c</a> <a id="957" class="Symbol">=</a> <a id="959" href="Relation.Binary.Reasoning.Syntax.html#1572" class="Function Operator">begin</a>
<a id="969" href="Algebra.Properties.IdempotentCommutativeMonoid.html#951" class="Bound">a</a> <a id="971" href="Algebra.Bundles.html#9368" class="Field Operator">∙</a> <a id="973" class="Symbol">(</a><a id="974" href="Algebra.Properties.IdempotentCommutativeMonoid.html#953" class="Bound">b</a> <a id="976" href="Algebra.Bundles.html#9368" class="Field Operator">∙</a> <a id="978" href="Algebra.Properties.IdempotentCommutativeMonoid.html#955" class="Bound">c</a><a id="979" class="Symbol">)</a> <a id="988" href="Relation.Binary.Reasoning.Syntax.html#7136" class="Function">≈⟨</a> <a id="991" href="Algebra.Structures.html#2009" class="Function">∙-congʳ</a> <a id="999" class="Symbol">(</a><a id="1000" href="Algebra.Structures.html#6061" class="Function">idem</a> <a id="1005" href="Algebra.Properties.IdempotentCommutativeMonoid.html#951" class="Bound">a</a><a id="1006" class="Symbol">)</a> <a id="1008" href="Relation.Binary.Reasoning.Syntax.html#7136" class="Function">⟨</a>
<a id="1014" class="Symbol">(</a><a id="1015" href="Algebra.Properties.IdempotentCommutativeMonoid.html#951" class="Bound">a</a> <a id="1017" href="Algebra.Bundles.html#9368" class="Field Operator">∙</a> <a id="1019" href="Algebra.Properties.IdempotentCommutativeMonoid.html#951" class="Bound">a</a><a id="1020" class="Symbol">)</a> <a id="1022" href="Algebra.Bundles.html#9368" class="Field Operator">∙</a> <a id="1024" class="Symbol">(</a><a id="1025" href="Algebra.Properties.IdempotentCommutativeMonoid.html#953" class="Bound">b</a> <a id="1027" href="Algebra.Bundles.html#9368" class="Field Operator">∙</a> <a id="1029" href="Algebra.Properties.IdempotentCommutativeMonoid.html#955" class="Bound">c</a><a id="1030" class="Symbol">)</a> <a id="1033" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">≈⟨</a> <a id="1036" href="Algebra.Properties.CommutativeSemigroup.html#833" class="Function">interchange</a> <a id="1048" class="Symbol">_</a> <a id="1050" class="Symbol">_</a> <a id="1052" class="Symbol">_</a> <a id="1054" class="Symbol">_</a> <a id="1056" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">⟩</a>
<a id="1062" class="Symbol">(</a><a id="1063" href="Algebra.Properties.IdempotentCommutativeMonoid.html#951" class="Bound">a</a> <a id="1065" href="Algebra.Bundles.html#9368" class="Field Operator">∙</a> <a id="1067" href="Algebra.Properties.IdempotentCommutativeMonoid.html#953" class="Bound">b</a><a id="1068" class="Symbol">)</a> <a id="1070" href="Algebra.Bundles.html#9368" class="Field Operator">∙</a> <a id="1072" class="Symbol">(</a><a id="1073" href="Algebra.Properties.IdempotentCommutativeMonoid.html#951" class="Bound">a</a> <a id="1075" href="Algebra.Bundles.html#9368" class="Field Operator">∙</a> <a id="1077" href="Algebra.Properties.IdempotentCommutativeMonoid.html#955" class="Bound">c</a><a id="1078" class="Symbol">)</a> <a id="1081" href="Relation.Binary.Reasoning.Syntax.html#12345" class="Function Operator">∎</a>

<a id="∙-distrʳ-∙"></a><a id="1084" href="Algebra.Properties.IdempotentCommutativeMonoid.html#1084" class="Function">∙-distrʳ-∙</a> <a id="1095" class="Symbol">:</a> <a id="1097" href="Algebra.Bundles.html#9368" class="Field Operator">_∙_</a> <a id="1101" href="Algebra.Definitions.html#3339" class="Function Operator">DistributesOverʳ</a> <a id="1118" href="Algebra.Bundles.html#9368" class="Field Operator">_∙_</a>
<a id="1122" href="Algebra.Properties.IdempotentCommutativeMonoid.html#1084" class="Function">∙-distrʳ-∙</a> <a id="1133" class="Symbol">=</a> <a id="1135" href="Algebra.Consequences.Setoid.html#7938" class="Function">comm∧distrˡ⇒distrʳ</a> <a id="1154" href="Algebra.Structures.html#1798" class="Function">∙-cong</a> <a id="1161" href="Algebra.Structures.html#5335" class="Function">comm</a> <a id="1166" href="Algebra.Properties.IdempotentCommutativeMonoid.html#902" class="Function">∙-distrˡ-∙</a>

<a id="∙-distr-∙"></a><a id="1178" href="Algebra.Properties.IdempotentCommutativeMonoid.html#1178" class="Function">∙-distr-∙</a> <a id="1188" class="Symbol">:</a> <a id="1190" href="Algebra.Bundles.html#9368" class="Field Operator">_∙_</a> <a id="1194" href="Algebra.Definitions.html#3458" class="Function Operator">DistributesOver</a> <a id="1210" href="Algebra.Bundles.html#9368" class="Field Operator">_∙_</a>
<a id="1214" href="Algebra.Properties.IdempotentCommutativeMonoid.html#1178" class="Function">∙-distr-∙</a> <a id="1224" class="Symbol">=</a> <a id="1226" href="Algebra.Consequences.Setoid.html#8511" class="Function">comm∧distrˡ⇒distr</a> <a id="1244" href="Algebra.Structures.html#1798" class="Function">∙-cong</a> <a id="1251" href="Algebra.Structures.html#5335" class="Function">comm</a> <a id="1256" href="Algebra.Properties.IdempotentCommutativeMonoid.html#902" class="Function">∙-distrˡ-∙</a>
</pre></body></html>
Loading

0 comments on commit 6759e81

Please sign in to comment.