Deploying to gh-pages from @ 5288e72 🚀

Author: github-merge-queue[bot]

master/Algebra.Properties.CommutativeMagma.Divisibility.html

@@ -18,7 +18,7 @@
 <a id="488" class="Comment">-- Re-exporting divisibility over monoids</a>
 
 <a id="531" class="Keyword">open</a> <a id="536" class="Keyword">import</a> <a id="543" href="Algebra.Properties.Monoid.Divisibility.html" class="Module">Algebra.Properties.Monoid.Divisibility</a> <a id="582" href="Algebra.Bundles.html#18200" class="Function">*-monoid</a> <a id="591" class="Keyword">public</a>
-  <a id="600" class="Keyword">renaming</a> <a id="609" class="Symbol">(</a><a id="610" href="Algebra.Properties.Monoid.Divisibility.html#971" class="Function Operator">ε∣_</a> <a id="614" class="Symbol">to</a> <a id="617" class="Function Operator">1∣_</a><a id="620" class="Symbol">)</a>
+  <a id="600" class="Keyword">renaming</a> <a id="609" class="Symbol">(</a><a id="610" href="Algebra.Properties.Monoid.Divisibility.html#3063" class="Function Operator">ε∣_</a> <a id="614" class="Symbol">to</a> <a id="617" class="Function Operator">1∣_</a><a id="620" class="Symbol">)</a>
 
 <a id="623" class="Comment">------------------------------------------------------------------------</a>
 <a id="696" class="Comment">-- Divisibility properties specific to semirings.</a>
@@ -32,7 +32,7 @@
 <a id="835" href="Algebra.Properties.Semiring.Divisibility.html#801" class="Function">0∣x⇒x≈0</a> <a id="843" class="Symbol">(</a><a id="844" href="Algebra.Properties.Semiring.Divisibility.html#844" class="Bound">q</a> <a id="846" href="Algebra.Definitions.RawMagma.html#1617" class="InductiveConstructor Operator">,</a> <a id="848" href="Algebra.Properties.Semiring.Divisibility.html#848" class="Bound">q*0≈x</a><a id="853" class="Symbol">)</a> <a id="855" class="Symbol">=</a> <a id="857" href="Relation.Binary.Structures.html#1648" class="Function">trans</a> <a id="863" class="Symbol">(</a><a id="864" href="Relation.Binary.Structures.html#1622" class="Function">sym</a> <a id="868" href="Algebra.Properties.Semiring.Divisibility.html#848" class="Bound">q*0≈x</a><a id="873" class="Symbol">)</a> <a id="875" class="Symbol">(</a><a id="876" href="Algebra.Structures.html#11865" class="Function">zeroʳ</a> <a id="882" href="Algebra.Properties.Semiring.Divisibility.html#844" class="Bound">q</a><a id="883" class="Symbol">)</a>
 
 <a id="x∣y∧y≉0⇒x≉0"></a><a id="886" href="Algebra.Properties.Semiring.Divisibility.html#886" class="Function">x∣y∧y≉0⇒x≉0</a> <a id="898" class="Symbol">:</a> <a id="900" class="Symbol">∀</a> <a id="902" class="Symbol">{</a><a id="903" href="Algebra.Properties.Semiring.Divisibility.html#903" class="Bound">x</a> <a id="905" href="Algebra.Properties.Semiring.Divisibility.html#905" class="Bound">y</a><a id="906" class="Symbol">}</a> <a id="908" class="Symbol">→</a> <a id="910" href="Algebra.Properties.Semiring.Divisibility.html#903" class="Bound">x</a> <a id="912" href="Algebra.Definitions.RawMagma.html#1891" class="Function Operator">∣</a> <a id="914" href="Algebra.Properties.Semiring.Divisibility.html#905" class="Bound">y</a> <a id="916" class="Symbol">→</a> <a id="918" href="Algebra.Properties.Semiring.Divisibility.html#905" class="Bound">y</a> <a id="920" href="Relation.Binary.Bundles.Raw.html#891" class="Function Operator">≉</a> <a id="922" href="Algebra.Bundles.html#18663" class="Field">0#</a> <a id="925" class="Symbol">→</a> <a id="927" href="Algebra.Properties.Semiring.Divisibility.html#903" class="Bound">x</a> <a id="929" href="Relation.Binary.Bundles.Raw.html#891" class="Function Operator">≉</a> <a id="931" href="Algebra.Bundles.html#18663" class="Field">0#</a>
-<a id="934" href="Algebra.Properties.Semiring.Divisibility.html#886" class="Function">x∣y∧y≉0⇒x≉0</a> <a id="946" href="Algebra.Properties.Semiring.Divisibility.html#946" class="Bound">x∣y</a> <a id="950" href="Algebra.Properties.Semiring.Divisibility.html#950" class="Bound">y≉0</a> <a id="954" href="Algebra.Properties.Semiring.Divisibility.html#954" class="Bound">x≈0</a> <a id="958" class="Symbol">=</a> <a id="960" href="Algebra.Properties.Semiring.Divisibility.html#950" class="Bound">y≉0</a> <a id="964" class="Symbol">(</a><a id="965" href="Algebra.Properties.Semiring.Divisibility.html#801" class="Function">0∣x⇒x≈0</a> <a id="973" class="Symbol">(</a><a id="974" href="Algebra.Properties.Magma.Divisibility.html#2799" class="Function">∣-respˡ</a> <a id="982" href="Algebra.Properties.Semiring.Divisibility.html#954" class="Bound">x≈0</a> <a id="986" href="Algebra.Properties.Semiring.Divisibility.html#946" class="Bound">x∣y</a><a id="989" class="Symbol">))</a>
+<a id="934" href="Algebra.Properties.Semiring.Divisibility.html#886" class="Function">x∣y∧y≉0⇒x≉0</a> <a id="946" href="Algebra.Properties.Semiring.Divisibility.html#946" class="Bound">x∣y</a> <a id="950" href="Algebra.Properties.Semiring.Divisibility.html#950" class="Bound">y≉0</a> <a id="954" href="Algebra.Properties.Semiring.Divisibility.html#954" class="Bound">x≈0</a> <a id="958" class="Symbol">=</a> <a id="960" href="Algebra.Properties.Semiring.Divisibility.html#950" class="Bound">y≉0</a> <a id="964" class="Symbol">(</a><a id="965" href="Algebra.Properties.Semiring.Divisibility.html#801" class="Function">0∣x⇒x≈0</a> <a id="973" class="Symbol">(</a><a id="974" href="Algebra.Properties.Magma.Divisibility.html#3316" class="Function">∣-respˡ</a> <a id="982" href="Algebra.Properties.Semiring.Divisibility.html#954" class="Bound">x≈0</a> <a id="986" href="Algebra.Properties.Semiring.Divisibility.html#946" class="Bound">x∣y</a><a id="989" class="Symbol">))</a>
 
 <a id="0∤1"></a><a id="993" href="Algebra.Properties.Semiring.Divisibility.html#993" class="Function">0∤1</a> <a id="997" class="Symbol">:</a> <a id="999" href="Algebra.Bundles.html#18663" class="Field">0#</a> <a id="1002" href="Relation.Binary.Bundles.Raw.html#891" class="Function Operator">≉</a> <a id="1004" href="Algebra.Bundles.html#18688" class="Field">1#</a> <a id="1007" class="Symbol">→</a> <a id="1009" href="Algebra.Bundles.html#18663" class="Field">0#</a> <a id="1012" href="Algebra.Definitions.RawMagma.html#1923" class="Function Operator">∤</a> <a id="1014" href="Algebra.Bundles.html#18688" class="Field">1#</a>
 <a id="1017" href="Algebra.Properties.Semiring.Divisibility.html#993" class="Function">0∤1</a> <a id="1021" href="Algebra.Properties.Semiring.Divisibility.html#1021" class="Bound">0≉1</a> <a id="1025" href="Algebra.Properties.Semiring.Divisibility.html#1025" class="Bound">0∣1</a> <a id="1029" class="Symbol">=</a> <a id="1031" href="Algebra.Properties.Semiring.Divisibility.html#1021" class="Bound">0≉1</a> <a id="1035" class="Symbol">(</a><a id="1036" href="Relation.Binary.Structures.html#1622" class="Function">sym</a> <a id="1040" class="Symbol">(</a><a id="1041" href="Algebra.Properties.Semiring.Divisibility.html#801" class="Function">0∣x⇒x≈0</a> <a id="1049" href="Algebra.Properties.Semiring.Divisibility.html#1025" class="Bound">0∣1</a><a id="1052" class="Symbol">))</a>

master/Algebra.Properties.CommutativeSemigroup.Divisibility.html

@@ -19,7 +19,7 @@
 
 <a id="553" class="Keyword">open</a> <a id="558" href="Algebra.Bundles.html#18455" class="Module">Semiring</a> <a id="567" href="Algebra.Properties.Semiring.Primality.html#387" class="Bound">R</a> <a id="569" class="Keyword">renaming</a> <a id="578" class="Symbol">(</a><a id="579" href="Algebra.Bundles.html#18551" class="Field">Carrier</a> <a id="587" class="Symbol">to</a> <a id="590" class="Field">A</a><a id="591" class="Symbol">)</a>
 <a id="593" class="Keyword">open</a> <a id="598" class="Keyword">import</a> <a id="605" href="Algebra.Properties.Semiring.Divisibility.html" class="Module">Algebra.Properties.Semiring.Divisibility</a> <a id="646" href="Algebra.Properties.Semiring.Primality.html#387" class="Bound">R</a>
-  <a id="650" class="Keyword">using</a> <a id="656" class="Symbol">(</a><a id="657" href="Algebra.Definitions.RawMagma.html#1891" class="Function Operator">_∣_</a><a id="660" class="Symbol">;</a> <a id="662" href="Algebra.Properties.Semigroup.Divisibility.html#787" class="Function">∣-trans</a><a id="669" class="Symbol">;</a> <a id="671" href="Algebra.Properties.Semiring.Divisibility.html#993" class="Function">0∤1</a><a id="674" class="Symbol">)</a>
+  <a id="650" class="Keyword">using</a> <a id="656" class="Symbol">(</a><a id="657" href="Algebra.Definitions.RawMagma.html#1891" class="Function Operator">_∣_</a><a id="660" class="Symbol">;</a> <a id="662" href="Algebra.Properties.Semigroup.Divisibility.html#2197" class="Function">∣-trans</a><a id="669" class="Symbol">;</a> <a id="671" href="Algebra.Properties.Semiring.Divisibility.html#993" class="Function">0∤1</a><a id="674" class="Symbol">)</a>
 
 <a id="677" class="Keyword">private</a>
   <a id="687" class="Keyword">variable</a>
@@ -39,7 +39,7 @@
 <a id="1070" href="Algebra.Properties.Semiring.Primality.html#1038" class="Function">Coprime-sym</a> <a id="1082" href="Algebra.Properties.Semiring.Primality.html#1082" class="Bound">coprime</a> <a id="1090" class="Symbol">=</a> <a id="1092" href="Function.Base.html#1638" class="Function">flip</a> <a id="1097" href="Algebra.Properties.Semiring.Primality.html#1082" class="Bound">coprime</a>
 
 <a id="∣1⇒Coprime"></a><a id="1106" href="Algebra.Properties.Semiring.Primality.html#1106" class="Function">∣1⇒Coprime</a> <a id="1117" class="Symbol">:</a> <a id="1119" class="Symbol">∀</a> <a id="1121" href="Algebra.Properties.Semiring.Primality.html#1121" class="Bound">y</a> <a id="1123" class="Symbol">→</a> <a id="1125" href="Algebra.Properties.Semiring.Primality.html#700" class="Generalizable">x</a> <a id="1127" href="Algebra.Definitions.RawMagma.html#1891" class="Function Operator">∣</a> <a id="1129" href="Algebra.Bundles.html#18688" class="Field">1#</a> <a id="1132" class="Symbol">→</a> <a id="1134" href="Algebra.Definitions.RawSemiring.html#1693" class="Function">Coprime</a> <a id="1142" href="Algebra.Properties.Semiring.Primality.html#700" class="Generalizable">x</a> <a id="1144" href="Algebra.Properties.Semiring.Primality.html#1121" class="Bound">y</a>
-<a id="1146" href="Algebra.Properties.Semiring.Primality.html#1106" class="Function">∣1⇒Coprime</a> <a id="1157" class="Symbol">_</a> <a id="1159" href="Algebra.Properties.Semiring.Primality.html#1159" class="Bound">x∣1</a> <a id="1163" href="Algebra.Properties.Semiring.Primality.html#1163" class="Bound">z∣x</a> <a id="1167" class="Symbol">_</a> <a id="1169" class="Symbol">=</a> <a id="1171" href="Algebra.Properties.Semigroup.Divisibility.html#787" class="Function">∣-trans</a> <a id="1179" href="Algebra.Properties.Semiring.Primality.html#1163" class="Bound">z∣x</a> <a id="1183" href="Algebra.Properties.Semiring.Primality.html#1159" class="Bound">x∣1</a>
+<a id="1146" href="Algebra.Properties.Semiring.Primality.html#1106" class="Function">∣1⇒Coprime</a> <a id="1157" class="Symbol">_</a> <a id="1159" href="Algebra.Properties.Semiring.Primality.html#1159" class="Bound">x∣1</a> <a id="1163" href="Algebra.Properties.Semiring.Primality.html#1163" class="Bound">z∣x</a> <a id="1167" class="Symbol">_</a> <a id="1169" class="Symbol">=</a> <a id="1171" href="Algebra.Properties.Semigroup.Divisibility.html#2197" class="Function">∣-trans</a> <a id="1179" href="Algebra.Properties.Semiring.Primality.html#1163" class="Bound">z∣x</a> <a id="1183" href="Algebra.Properties.Semiring.Primality.html#1159" class="Bound">x∣1</a>
 
 <a id="1188" class="Comment">------------------------------------------------------------------------</a>
 <a id="1261" class="Comment">-- Properties of Irreducible</a>