Skip to content

Commit

Permalink
Deploying to gh-pages from @ 0cccb39 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@github-merge-queue
github-merge-queue[bot] committed Jan 23, 2025
1 parent 9a0980f commit d3db8d3
Show file tree
Hide file tree
Showing 12 changed files with 288 additions and 182 deletions.
129 changes: 75 additions & 54 deletions master/Algebra.Definitions.RawMagma.html
View file

Large diffs are not rendered by default.

14 changes: 7 additions & 7 deletions master/Algebra.Definitions.RawSemiring.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,8 +32,8 @@

<a id="962" class="Keyword">open</a> <a id="967" class="Keyword">import</a> <a id="974" href="Algebra.Definitions.RawMonoid.html" class="Module">Algebra.Definitions.RawMonoid</a> <a id="1004" href="Algebra.Bundles.Raw.html#4066" class="Function">*-rawMonoid</a> <a id="1016" class="Symbol">as</a> <a id="Mult"></a><a id="1019" href="Algebra.Definitions.RawSemiring.html#1019" class="Module">Mult</a> <a id="1024" class="Keyword">public</a>
<a id="1033" class="Keyword">using</a>
<a id="1041" class="Symbol">(</a> <a id="1043" href="Algebra.Definitions.RawMagma.html#1883" class="Function Operator">_∣_</a>
<a id="1049" class="Symbol">;</a> <a id="1051" href="Algebra.Definitions.RawMagma.html#1915" class="Function Operator">_∤_</a>
<a id="1041" class="Symbol">(</a> <a id="1043" href="Algebra.Definitions.RawMagma.html#1878" class="Function Operator">_∣_</a>
<a id="1049" class="Symbol">;</a> <a id="1051" href="Algebra.Definitions.RawMagma.html#1910" class="Function Operator">_∤_</a>
<a id="1057" class="Symbol">)</a>
<a id="1061" class="Keyword">renaming</a>
<a id="1072" class="Symbol">(</a> <a id="1074" href="Algebra.Definitions.RawMonoid.html#2111" class="Function">sum</a> <a id="1078" class="Symbol">to</a> <a id="1081" class="Function">product</a>
Expand Down Expand Up @@ -70,18 +70,18 @@
<a id="1679" class="Comment">-- Primality</a>

<a id="Coprime"></a><a id="1693" href="Algebra.Definitions.RawSemiring.html#1693" class="Function">Coprime</a> <a id="1701" class="Symbol">:</a> <a id="1703" href="Relation.Binary.Core.html#896" class="Function">Rel</a> <a id="1707" href="Algebra.Definitions.RawSemiring.html#608" class="Field">A</a> <a id="1709" class="Symbol">(</a><a id="1710" href="Algebra.Definitions.RawSemiring.html#534" class="Bound">a</a> <a id="1712" href="Agda.Primitive.html#961" class="Primitive Operator">⊔</a> <a id="1714" href="Algebra.Definitions.RawSemiring.html#536" class="Bound">ℓ</a><a id="1715" class="Symbol">)</a>
<a id="1717" href="Algebra.Definitions.RawSemiring.html#1693" class="Function">Coprime</a> <a id="1725" href="Algebra.Definitions.RawSemiring.html#1725" class="Bound">x</a> <a id="1727" href="Algebra.Definitions.RawSemiring.html#1727" class="Bound">y</a> <a id="1729" class="Symbol">=</a> <a id="1731" class="Symbol">∀</a> <a id="1733" class="Symbol">{</a><a id="1734" href="Algebra.Definitions.RawSemiring.html#1734" class="Bound">z</a><a id="1735" class="Symbol">}</a> <a id="1737" class="Symbol">→</a> <a id="1739" href="Algebra.Definitions.RawSemiring.html#1734" class="Bound">z</a> <a id="1741" href="Algebra.Definitions.RawMagma.html#1883" class="Function Operator">∣</a> <a id="1743" href="Algebra.Definitions.RawSemiring.html#1725" class="Bound">x</a> <a id="1745" class="Symbol">→</a> <a id="1747" href="Algebra.Definitions.RawSemiring.html#1734" class="Bound">z</a> <a id="1749" href="Algebra.Definitions.RawMagma.html#1883" class="Function Operator">∣</a> <a id="1751" href="Algebra.Definitions.RawSemiring.html#1727" class="Bound">y</a> <a id="1753" class="Symbol">→</a> <a id="1755" href="Algebra.Definitions.RawSemiring.html#1734" class="Bound">z</a> <a id="1757" href="Algebra.Definitions.RawMagma.html#1883" class="Function Operator">∣</a> <a id="1759" href="Algebra.Bundles.Raw.html#3808" class="Field">1#</a>
<a id="1717" href="Algebra.Definitions.RawSemiring.html#1693" class="Function">Coprime</a> <a id="1725" href="Algebra.Definitions.RawSemiring.html#1725" class="Bound">x</a> <a id="1727" href="Algebra.Definitions.RawSemiring.html#1727" class="Bound">y</a> <a id="1729" class="Symbol">=</a> <a id="1731" class="Symbol">∀</a> <a id="1733" class="Symbol">{</a><a id="1734" href="Algebra.Definitions.RawSemiring.html#1734" class="Bound">z</a><a id="1735" class="Symbol">}</a> <a id="1737" class="Symbol">→</a> <a id="1739" href="Algebra.Definitions.RawSemiring.html#1734" class="Bound">z</a> <a id="1741" href="Algebra.Definitions.RawMagma.html#1878" class="Function Operator">∣</a> <a id="1743" href="Algebra.Definitions.RawSemiring.html#1725" class="Bound">x</a> <a id="1745" class="Symbol">→</a> <a id="1747" href="Algebra.Definitions.RawSemiring.html#1734" class="Bound">z</a> <a id="1749" href="Algebra.Definitions.RawMagma.html#1878" class="Function Operator">∣</a> <a id="1751" href="Algebra.Definitions.RawSemiring.html#1727" class="Bound">y</a> <a id="1753" class="Symbol">→</a> <a id="1755" href="Algebra.Definitions.RawSemiring.html#1734" class="Bound">z</a> <a id="1757" href="Algebra.Definitions.RawMagma.html#1878" class="Function Operator">∣</a> <a id="1759" href="Algebra.Bundles.Raw.html#3808" class="Field">1#</a>

<a id="1763" class="Keyword">record</a> <a id="Irreducible"></a><a id="1770" href="Algebra.Definitions.RawSemiring.html#1770" class="Record">Irreducible</a> <a id="1782" class="Symbol">(</a><a id="1783" href="Algebra.Definitions.RawSemiring.html#1783" class="Bound">p</a> <a id="1785" class="Symbol">:</a> <a id="1787" href="Algebra.Definitions.RawSemiring.html#608" class="Field">A</a><a id="1788" class="Symbol">)</a> <a id="1790" class="Symbol">:</a> <a id="1792" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="1796" class="Symbol">(</a><a id="1797" href="Algebra.Definitions.RawSemiring.html#534" class="Bound">a</a> <a id="1799" href="Agda.Primitive.html#961" class="Primitive Operator">⊔</a> <a id="1801" href="Algebra.Definitions.RawSemiring.html#536" class="Bound">ℓ</a><a id="1802" class="Symbol">)</a> <a id="1804" class="Keyword">where</a>
<a id="1812" class="Keyword">constructor</a> <a id="mkIrred"></a><a id="1824" href="Algebra.Definitions.RawSemiring.html#1824" class="InductiveConstructor">mkIrred</a>
<a id="1834" class="Keyword">field</a>
<a id="Irreducible.p∤1"></a><a id="1844" href="Algebra.Definitions.RawSemiring.html#1844" class="Field">p∤1</a> <a id="1854" class="Symbol">:</a> <a id="1856" href="Algebra.Definitions.RawSemiring.html#1783" class="Bound">p</a> <a id="1858" href="Algebra.Definitions.RawMagma.html#1915" class="Function Operator">∤</a> <a id="1860" href="Algebra.Bundles.Raw.html#3808" class="Field">1#</a>
<a id="Irreducible.split-∣1"></a><a id="1867" href="Algebra.Definitions.RawSemiring.html#1867" class="Field">split-∣1</a> <a id="1876" class="Symbol">:</a> <a id="1878" class="Symbol">∀</a> <a id="1880" class="Symbol">{</a><a id="1881" href="Algebra.Definitions.RawSemiring.html#1881" class="Bound">x</a> <a id="1883" href="Algebra.Definitions.RawSemiring.html#1883" class="Bound">y</a><a id="1884" class="Symbol">}</a> <a id="1886" class="Symbol">→</a> <a id="1888" href="Algebra.Definitions.RawSemiring.html#1783" class="Bound">p</a> <a id="1890" href="Algebra.Bundles.Raw.html#3706" class="Field Operator">≈</a> <a id="1892" class="Symbol">(</a><a id="1893" href="Algebra.Definitions.RawSemiring.html#1881" class="Bound">x</a> <a id="1895" href="Algebra.Bundles.Raw.html#3760" class="Field Operator">*</a> <a id="1897" href="Algebra.Definitions.RawSemiring.html#1883" class="Bound">y</a><a id="1898" class="Symbol">)</a> <a id="1900" class="Symbol">→</a> <a id="1902" href="Algebra.Definitions.RawSemiring.html#1881" class="Bound">x</a> <a id="1904" href="Algebra.Definitions.RawMagma.html#1883" class="Function Operator">∣</a> <a id="1906" href="Algebra.Bundles.Raw.html#3808" class="Field">1#</a> <a id="1909" href="Data.Sum.Base.html#625" class="Datatype Operator">⊎</a> <a id="1911" href="Algebra.Definitions.RawSemiring.html#1883" class="Bound">y</a> <a id="1913" href="Algebra.Definitions.RawMagma.html#1883" class="Function Operator">∣</a> <a id="1915" href="Algebra.Bundles.Raw.html#3808" class="Field">1#</a>
<a id="Irreducible.p∤1"></a><a id="1844" href="Algebra.Definitions.RawSemiring.html#1844" class="Field">p∤1</a> <a id="1854" class="Symbol">:</a> <a id="1856" href="Algebra.Definitions.RawSemiring.html#1783" class="Bound">p</a> <a id="1858" href="Algebra.Definitions.RawMagma.html#1910" class="Function Operator">∤</a> <a id="1860" href="Algebra.Bundles.Raw.html#3808" class="Field">1#</a>
<a id="Irreducible.split-∣1"></a><a id="1867" href="Algebra.Definitions.RawSemiring.html#1867" class="Field">split-∣1</a> <a id="1876" class="Symbol">:</a> <a id="1878" class="Symbol">∀</a> <a id="1880" class="Symbol">{</a><a id="1881" href="Algebra.Definitions.RawSemiring.html#1881" class="Bound">x</a> <a id="1883" href="Algebra.Definitions.RawSemiring.html#1883" class="Bound">y</a><a id="1884" class="Symbol">}</a> <a id="1886" class="Symbol">→</a> <a id="1888" href="Algebra.Definitions.RawSemiring.html#1783" class="Bound">p</a> <a id="1890" href="Algebra.Bundles.Raw.html#3706" class="Field Operator">≈</a> <a id="1892" class="Symbol">(</a><a id="1893" href="Algebra.Definitions.RawSemiring.html#1881" class="Bound">x</a> <a id="1895" href="Algebra.Bundles.Raw.html#3760" class="Field Operator">*</a> <a id="1897" href="Algebra.Definitions.RawSemiring.html#1883" class="Bound">y</a><a id="1898" class="Symbol">)</a> <a id="1900" class="Symbol">→</a> <a id="1902" href="Algebra.Definitions.RawSemiring.html#1881" class="Bound">x</a> <a id="1904" href="Algebra.Definitions.RawMagma.html#1878" class="Function Operator">∣</a> <a id="1906" href="Algebra.Bundles.Raw.html#3808" class="Field">1#</a> <a id="1909" href="Data.Sum.Base.html#625" class="Datatype Operator">⊎</a> <a id="1911" href="Algebra.Definitions.RawSemiring.html#1883" class="Bound">y</a> <a id="1913" href="Algebra.Definitions.RawMagma.html#1878" class="Function Operator">∣</a> <a id="1915" href="Algebra.Bundles.Raw.html#3808" class="Field">1#</a>

<a id="1919" class="Keyword">record</a> <a id="Prime"></a><a id="1926" href="Algebra.Definitions.RawSemiring.html#1926" class="Record">Prime</a> <a id="1932" class="Symbol">(</a><a id="1933" href="Algebra.Definitions.RawSemiring.html#1933" class="Bound">p</a> <a id="1935" class="Symbol">:</a> <a id="1937" href="Algebra.Definitions.RawSemiring.html#608" class="Field">A</a><a id="1938" class="Symbol">)</a> <a id="1940" class="Symbol">:</a> <a id="1942" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="1946" class="Symbol">(</a><a id="1947" href="Algebra.Definitions.RawSemiring.html#534" class="Bound">a</a> <a id="1949" href="Agda.Primitive.html#961" class="Primitive Operator">⊔</a> <a id="1951" href="Algebra.Definitions.RawSemiring.html#536" class="Bound">ℓ</a><a id="1952" class="Symbol">)</a> <a id="1954" class="Keyword">where</a>
<a id="1962" class="Keyword">constructor</a> <a id="mkPrime"></a><a id="1974" href="Algebra.Definitions.RawSemiring.html#1974" class="InductiveConstructor">mkPrime</a>
<a id="1984" class="Keyword">field</a>
<a id="Prime.p≉0"></a><a id="1994" href="Algebra.Definitions.RawSemiring.html#1994" class="Field">p≉0</a> <a id="2002" class="Symbol">:</a> <a id="2004" href="Algebra.Definitions.RawSemiring.html#1933" class="Bound">p</a> <a id="2006" href="Relation.Binary.Bundles.Raw.html#891" class="Function Operator">≉</a> <a id="2008" href="Algebra.Bundles.Raw.html#3786" class="Field">0#</a>
<a id="Prime.p∤1"></a><a id="2015" href="Algebra.Definitions.RawSemiring.html#2015" class="Field">p∤1</a> <a id="2023" class="Symbol">:</a> <a id="2025" href="Algebra.Definitions.RawSemiring.html#1933" class="Bound">p</a> <a id="2027" href="Algebra.Definitions.RawMagma.html#1915" class="Function Operator">∤</a> <a id="2029" href="Algebra.Bundles.Raw.html#3808" class="Field">1#</a>
<a id="Prime.split-∣"></a><a id="2036" href="Algebra.Definitions.RawSemiring.html#2036" class="Field">split-∣</a> <a id="2044" class="Symbol">:</a> <a id="2046" class="Symbol">∀</a> <a id="2048" class="Symbol">{</a><a id="2049" href="Algebra.Definitions.RawSemiring.html#2049" class="Bound">x</a> <a id="2051" href="Algebra.Definitions.RawSemiring.html#2051" class="Bound">y</a><a id="2052" class="Symbol">}</a> <a id="2054" class="Symbol">→</a> <a id="2056" href="Algebra.Definitions.RawSemiring.html#1933" class="Bound">p</a> <a id="2058" href="Algebra.Definitions.RawMagma.html#1883" class="Function Operator">∣</a> <a id="2060" href="Algebra.Definitions.RawSemiring.html#2049" class="Bound">x</a> <a id="2062" href="Algebra.Bundles.Raw.html#3760" class="Field Operator">*</a> <a id="2064" href="Algebra.Definitions.RawSemiring.html#2051" class="Bound">y</a> <a id="2066" class="Symbol">→</a> <a id="2068" href="Algebra.Definitions.RawSemiring.html#1933" class="Bound">p</a> <a id="2070" href="Algebra.Definitions.RawMagma.html#1883" class="Function Operator">∣</a> <a id="2072" href="Algebra.Definitions.RawSemiring.html#2049" class="Bound">x</a> <a id="2074" href="Data.Sum.Base.html#625" class="Datatype Operator">⊎</a> <a id="2076" href="Algebra.Definitions.RawSemiring.html#1933" class="Bound">p</a> <a id="2078" href="Algebra.Definitions.RawMagma.html#1883" class="Function Operator">∣</a> <a id="2080" href="Algebra.Definitions.RawSemiring.html#2051" class="Bound">y</a>
<a id="Prime.p∤1"></a><a id="2015" href="Algebra.Definitions.RawSemiring.html#2015" class="Field">p∤1</a> <a id="2023" class="Symbol">:</a> <a id="2025" href="Algebra.Definitions.RawSemiring.html#1933" class="Bound">p</a> <a id="2027" href="Algebra.Definitions.RawMagma.html#1910" class="Function Operator">∤</a> <a id="2029" href="Algebra.Bundles.Raw.html#3808" class="Field">1#</a>
<a id="Prime.split-∣"></a><a id="2036" href="Algebra.Definitions.RawSemiring.html#2036" class="Field">split-∣</a> <a id="2044" class="Symbol">:</a> <a id="2046" class="Symbol">∀</a> <a id="2048" class="Symbol">{</a><a id="2049" href="Algebra.Definitions.RawSemiring.html#2049" class="Bound">x</a> <a id="2051" href="Algebra.Definitions.RawSemiring.html#2051" class="Bound">y</a><a id="2052" class="Symbol">}</a> <a id="2054" class="Symbol">→</a> <a id="2056" href="Algebra.Definitions.RawSemiring.html#1933" class="Bound">p</a> <a id="2058" href="Algebra.Definitions.RawMagma.html#1878" class="Function Operator">∣</a> <a id="2060" href="Algebra.Definitions.RawSemiring.html#2049" class="Bound">x</a> <a id="2062" href="Algebra.Bundles.Raw.html#3760" class="Field Operator">*</a> <a id="2064" href="Algebra.Definitions.RawSemiring.html#2051" class="Bound">y</a> <a id="2066" class="Symbol">→</a> <a id="2068" href="Algebra.Definitions.RawSemiring.html#1933" class="Bound">p</a> <a id="2070" href="Algebra.Definitions.RawMagma.html#1878" class="Function Operator">∣</a> <a id="2072" href="Algebra.Definitions.RawSemiring.html#2049" class="Bound">x</a> <a id="2074" href="Data.Sum.Base.html#625" class="Datatype Operator">⊎</a> <a id="2076" href="Algebra.Definitions.RawSemiring.html#1933" class="Bound">p</a> <a id="2078" href="Algebra.Definitions.RawMagma.html#1878" class="Function Operator">∣</a> <a id="2080" href="Algebra.Definitions.RawSemiring.html#2051" class="Bound">y</a>
</pre></body></html>
Loading

0 comments on commit d3db8d3

Please sign in to comment.