Deploying to gh-pages from @ ab4fbd2 🚀

Author: github-merge-queue[bot]

master/Algebra.Properties.Semiring.Binomial.html

@@ -22,7 +22,7 @@
 <a id="615" class="Keyword">open</a> <a id="620" class="Keyword">import</a> <a id="627" href="Data.Nat.Combinatorics.html" class="Module">Data.Nat.Combinatorics</a>
   <a id="652" class="Keyword">using</a> <a id="658" class="Symbol">(</a><a id="659" href="Data.Nat.Combinatorics.Base.html#1622" class="Function Operator">_C_</a><a id="662" class="Symbol">;</a> <a id="664" href="Data.Nat.Combinatorics.html#2974" class="Function">nCn≡1</a><a id="669" class="Symbol">;</a> <a id="671" href="Data.Nat.Combinatorics.html#3195" class="Function">nC1≡n</a><a id="676" class="Symbol">;</a> <a id="678" href="Data.Nat.Combinatorics.html#4831" class="Function">nCk+nC[k+1]≡[n+1]C[k+1]</a><a id="701" class="Symbol">)</a>
 <a id="703" class="Keyword">open</a> <a id="708" class="Keyword">import</a> <a id="715" href="Data.Nat.Properties.html" class="Module">Data.Nat.Properties</a> <a id="735" class="Symbol">as</a> <a id="738" class="Module">ℕ</a>
-  <a id="742" class="Keyword">using</a> <a id="748" class="Symbol">(</a><a id="749" href="Data.Nat.Properties.html#5072" class="Function">&lt;⇒&lt;ᵇ</a><a id="753" class="Symbol">;</a> <a id="755" href="Data.Nat.Properties.html#13416" class="Function">n&lt;1+n</a><a id="760" class="Symbol">;</a> <a id="762" href="Data.Nat.Properties.html#46995" class="Function">n∸n≡0</a><a id="767" class="Symbol">;</a> <a id="769" href="Data.Nat.Properties.html#47511" class="Function">∸-suc</a><a id="774" class="Symbol">)</a>
+  <a id="742" class="Keyword">using</a> <a id="748" class="Symbol">(</a><a id="749" href="Data.Nat.Properties.html#5072" class="Function">&lt;⇒&lt;ᵇ</a><a id="753" class="Symbol">;</a> <a id="755" href="Data.Nat.Properties.html#13416" class="Function">n&lt;1+n</a><a id="760" class="Symbol">;</a> <a id="762" href="Data.Nat.Properties.html#47190" class="Function">n∸n≡0</a><a id="767" class="Symbol">;</a> <a id="769" href="Data.Nat.Properties.html#47706" class="Function">∸-suc</a><a id="774" class="Symbol">)</a>
 <a id="776" class="Keyword">open</a> <a id="781" class="Keyword">import</a> <a id="788" href="Data.Fin.Base.html" class="Module">Data.Fin.Base</a> <a id="802" class="Symbol">as</a> <a id="805" class="Module">Fin</a>
   <a id="811" class="Keyword">using</a> <a id="817" class="Symbol">(</a><a id="818" href="Data.Fin.Base.html#1132" class="Datatype">Fin</a><a id="821" class="Symbol">;</a> <a id="823" href="Data.Fin.Base.html#1154" class="InductiveConstructor">zero</a><a id="827" class="Symbol">;</a> <a id="829" href="Data.Fin.Base.html#1175" class="InductiveConstructor">suc</a><a id="832" class="Symbol">;</a> <a id="834" href="Data.Fin.Base.html#1240" class="Function">toℕ</a><a id="837" class="Symbol">;</a> <a id="839" href="Data.Fin.Base.html#1825" class="Function">fromℕ</a><a id="844" class="Symbol">;</a> <a id="846" href="Data.Fin.Base.html#3055" class="Function">inject₁</a><a id="853" class="Symbol">)</a>
 <a id="855" class="Keyword">open</a> <a id="860" class="Keyword">import</a> <a id="867" href="Data.Fin.Patterns.html" class="Module">Data.Fin.Patterns</a> <a id="885" class="Keyword">using</a> <a id="891" class="Symbol">(</a><a id="892" href="Data.Fin.Patterns.html#422" class="InductiveConstructor">0F</a><a id="894" class="Symbol">)</a>
@@ -150,7 +150,7 @@
     <a id="5378" href="Algebra.Properties.Semiring.Binomial.html#5358" class="Function">k≡j</a> <a id="5382" class="Symbol">=</a> <a id="5384" href="Data.Fin.Properties.html#16316" class="Function">toℕ-inject₁</a> <a id="5396" href="Algebra.Properties.Semiring.Binomial.html#4569" class="Bound">j</a>
 
     <a id="5403" href="Algebra.Properties.Semiring.Binomial.html#5403" class="Function">[n-k]≡[n-j]</a> <a id="5415" class="Symbol">:</a> <a id="5417" href="Algebra.Properties.Semiring.Binomial.html#5221" class="Function">[n-k]</a> <a id="5423" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">≡</a> <a id="5425" href="Algebra.Properties.Semiring.Binomial.html#5297" class="Function">[n-j]</a>
-    <a id="5435" href="Algebra.Properties.Semiring.Binomial.html#5403" class="Function">[n-k]≡[n-j]</a> <a id="5447" class="Symbol">=</a> <a id="5449" href="Relation.Binary.PropositionalEquality.Core.html#2080" class="Function">≡.trans</a> <a id="5457" class="Symbol">(</a><a id="5458" href="Relation.Binary.PropositionalEquality.Core.html#1481" class="Function">cong</a> <a id="5463" class="Symbol">(</a><a id="5464" href="Algebra.Properties.Semiring.Binomial.html#4566" class="Bound">n</a> <a id="5466" href="Data.Nat.Base.html#4462" class="Primitive Operator">∸_</a><a id="5468" class="Symbol">)</a> <a id="5470" href="Algebra.Properties.Semiring.Binomial.html#5358" class="Function">k≡j</a><a id="5473" class="Symbol">)</a> <a id="5475" class="Symbol">(</a><a id="5476" href="Data.Nat.Properties.html#47511" class="Function">∸-suc</a> <a id="5482" class="Symbol">(</a><a id="5483" href="Data.Fin.Properties.html#6596" class="Function">toℕ&lt;n</a> <a id="5489" href="Algebra.Properties.Semiring.Binomial.html#4569" class="Bound">j</a><a id="5490" class="Symbol">))</a>
+    <a id="5435" href="Algebra.Properties.Semiring.Binomial.html#5403" class="Function">[n-k]≡[n-j]</a> <a id="5447" class="Symbol">=</a> <a id="5449" href="Relation.Binary.PropositionalEquality.Core.html#2080" class="Function">≡.trans</a> <a id="5457" class="Symbol">(</a><a id="5458" href="Relation.Binary.PropositionalEquality.Core.html#1481" class="Function">cong</a> <a id="5463" class="Symbol">(</a><a id="5464" href="Algebra.Properties.Semiring.Binomial.html#4566" class="Bound">n</a> <a id="5466" href="Data.Nat.Base.html#4462" class="Primitive Operator">∸_</a><a id="5468" class="Symbol">)</a> <a id="5470" href="Algebra.Properties.Semiring.Binomial.html#5358" class="Function">k≡j</a><a id="5473" class="Symbol">)</a> <a id="5475" class="Symbol">(</a><a id="5476" href="Data.Nat.Properties.html#47706" class="Function">∸-suc</a> <a id="5482" class="Symbol">(</a><a id="5483" href="Data.Fin.Properties.html#6596" class="Function">toℕ&lt;n</a> <a id="5489" href="Algebra.Properties.Semiring.Binomial.html#4569" class="Bound">j</a><a id="5490" class="Symbol">))</a>
 
 <a id="5494" class="Comment">------------------------------------------------------------------------</a>
 <a id="5567" class="Comment">-- Now, a lemma characterising the sum of the term₁ and term₂ expressions</a>
@@ -177,7 +177,7 @@
 <a id="6400" class="Comment">{- remembering that i = fromℕ n, definitionally -}</a>
   <a id="6453" class="Keyword">rewrite</a> <a id="6461" href="Data.Fin.Properties.html#7620" class="Function">toℕ-fromℕ</a> <a id="6471" href="Algebra.Properties.Semiring.Binomial.html#6397" class="Bound">n</a>
     <a id="6477" class="Symbol">|</a> <a id="6479" href="Data.Nat.Combinatorics.html#2974" class="Function">nCn≡1</a> <a id="6485" href="Algebra.Properties.Semiring.Binomial.html#6397" class="Bound">n</a>
-    <a id="6491" class="Symbol">|</a> <a id="6493" href="Data.Nat.Properties.html#46995" class="Function">n∸n≡0</a> <a id="6499" href="Algebra.Properties.Semiring.Binomial.html#6397" class="Bound">n</a>
+    <a id="6491" class="Symbol">|</a> <a id="6493" href="Data.Nat.Properties.html#47190" class="Function">n∸n≡0</a> <a id="6499" href="Algebra.Properties.Semiring.Binomial.html#6397" class="Bound">n</a>
     <a id="6505" class="Symbol">|</a> <a id="6507" href="Algebra.Properties.Semiring.Binomial.html#5652" class="Function">n&lt;ᵇ1+n</a> <a id="6514" href="Algebra.Properties.Semiring.Binomial.html#6397" class="Bound">n</a>
     <a id="6520" class="Symbol">=</a> <a id="6522" href="Relation.Binary.Reasoning.Syntax.html#1572" class="Function Operator">begin</a>
   <a id="6530" href="Algebra.Properties.Semiring.Binomial.html#497" class="Bound">x</a> <a id="6532" href="Algebra.Bundles.html#18634" class="Field Operator">*</a> <a id="6534" class="Symbol">((</a><a id="6536" href="Algebra.Properties.Semiring.Binomial.html#497" class="Bound">x</a> <a id="6538" href="Algebra.Definitions.RawSemiring.html#1256" class="Function Operator">^</a> <a id="6540" href="Algebra.Properties.Semiring.Binomial.html#6397" class="Bound">n</a> <a id="6542" href="Algebra.Bundles.html#18634" class="Field Operator">*</a> <a id="6544" href="Algebra.Bundles.html#18688" class="Field">1#</a><a id="6546" class="Symbol">)</a> <a id="6548" href="Algebra.Bundles.html#18605" class="Field Operator">+</a> <a id="6550" href="Algebra.Bundles.html#18663" class="Field">0#</a><a id="6552" class="Symbol">)</a> <a id="6554" href="Algebra.Bundles.html#18605" class="Field Operator">+</a> <a id="6556" href="Algebra.Bundles.html#18663" class="Field">0#</a> <a id="6559" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">≈⟨</a> <a id="6562" href="Algebra.Structures.html#15099" class="Function">+-identityʳ</a> <a id="6574" class="Symbol">_</a> <a id="6576" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">⟩</a>

master/Algebra.Properties.Semiring.Exp.TCOptimised.html

@@ -13,7 +13,7 @@
   <a id="387" class="Symbol">{</a><a id="388" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#388" class="Bound">a</a> <a id="390" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#390" class="Bound">ℓ</a><a id="391" class="Symbol">}</a> <a id="393" class="Symbol">(</a><a id="394" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#394" class="Bound">S</a> <a id="396" class="Symbol">:</a> <a id="398" href="Algebra.Bundles.html#18455" class="Record">Semiring</a> <a id="407" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#388" class="Bound">a</a> <a id="409" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#390" class="Bound">ℓ</a><a id="410" class="Symbol">)</a> <a id="412" class="Keyword">where</a>
 
 <a id="419" class="Keyword">open</a> <a id="424" class="Keyword">import</a> <a id="431" href="Data.Nat.Base.html" class="Module">Data.Nat.Base</a> <a id="445" class="Symbol">as</a> <a id="448" class="Module">ℕ</a> <a id="450" class="Keyword">using</a> <a id="456" class="Symbol">(</a><a id="457" href="Agda.Builtin.Nat.html#221" class="InductiveConstructor">zero</a><a id="461" class="Symbol">;</a> <a id="463" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a><a id="466" class="Symbol">)</a>
-<a id="468" class="Keyword">import</a> <a id="475" href="Data.Nat.Properties.html" class="Module">Data.Nat.Properties</a> <a id="495" class="Symbol">as</a> <a id="498" class="Module">ℕ</a> <a id="500" class="Keyword">using</a> <a id="506" class="Symbol">(</a><a id="507" href="Data.Nat.Properties.html#15478" class="Function">+-suc</a><a id="512" class="Symbol">;</a> <a id="514" href="Data.Nat.Properties.html#22523" class="Function">*-comm</a><a id="520" class="Symbol">)</a>
+<a id="468" class="Keyword">import</a> <a id="475" href="Data.Nat.Properties.html" class="Module">Data.Nat.Properties</a> <a id="495" class="Symbol">as</a> <a id="498" class="Module">ℕ</a> <a id="500" class="Keyword">using</a> <a id="506" class="Symbol">(</a><a id="507" href="Data.Nat.Properties.html#15478" class="Function">+-suc</a><a id="512" class="Symbol">;</a> <a id="514" href="Data.Nat.Properties.html#22718" class="Function">*-comm</a><a id="520" class="Symbol">)</a>
 <a id="522" class="Keyword">open</a> <a id="527" class="Keyword">import</a> <a id="534" href="Relation.Binary.Core.html" class="Module">Relation.Binary.Core</a> <a id="555" class="Keyword">using</a> <a id="561" class="Symbol">(</a><a id="562" href="Relation.Binary.Core.html#1577" class="Function Operator">_Preserves_⟶_</a><a id="575" class="Symbol">;</a> <a id="577" href="Relation.Binary.Core.html#1703" class="Function Operator">_Preserves₂_⟶_⟶_</a><a id="593" class="Symbol">)</a>
 <a id="595" class="Keyword">open</a> <a id="600" class="Keyword">import</a> <a id="607" href="Relation.Binary.PropositionalEquality.Core.html" class="Module">Relation.Binary.PropositionalEquality.Core</a> <a id="650" class="Keyword">using</a> <a id="656" class="Symbol">(</a><a id="657" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">_≡_</a><a id="660" class="Symbol">)</a>
 <a id="662" class="Keyword">open</a> <a id="667" href="Algebra.Bundles.html#18455" class="Module">Semiring</a> <a id="676" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#394" class="Bound">S</a> <a id="678" class="Keyword">renaming</a> <a id="687" class="Symbol">(</a><a id="688" href="Algebra.Structures.html#16158" class="Function">zero</a> <a id="693" class="Symbol">to</a> <a id="696" class="Function">*-zero</a><a id="702" class="Symbol">)</a>
@@ -44,5 +44,5 @@
 
 <a id="1458" class="Comment">-- (xᵐ)ⁿ≈xᵐ*ⁿ</a>
 <a id="^-assocʳ"></a><a id="1472" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1472" class="Function">^-assocʳ</a> <a id="1481" class="Symbol">:</a> <a id="1483" class="Symbol">∀</a> <a id="1485" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1485" class="Bound">x</a> <a id="1487" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1487" class="Bound">m</a> <a id="1489" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1489" class="Bound">n</a> <a id="1491" class="Symbol">→</a> <a id="1493" class="Symbol">(</a><a id="1494" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1485" class="Bound">x</a> <a id="1496" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1116" class="Function Operator">^</a> <a id="1498" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1487" class="Bound">m</a><a id="1499" class="Symbol">)</a> <a id="1501" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1116" class="Function Operator">^</a> <a id="1503" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1489" class="Bound">n</a> <a id="1505" href="Algebra.Bundles.html#18574" class="Field Operator">≈</a> <a id="1507" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1485" class="Bound">x</a> <a id="1509" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1116" class="Function Operator">^</a> <a id="1511" class="Symbol">(</a><a id="1512" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1487" class="Bound">m</a> <a id="1514" href="Agda.Builtin.Nat.html#539" class="Primitive Operator">ℕ.*</a> <a id="1518" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1489" class="Bound">n</a><a id="1519" class="Symbol">)</a>
-<a id="1521" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1472" class="Function">^-assocʳ</a> <a id="1530" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1530" class="Bound">x</a> <a id="1532" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1532" class="Bound">m</a> <a id="1534" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1534" class="Bound">n</a> <a id="1536" class="Keyword">rewrite</a> <a id="1544" href="Data.Nat.Properties.html#22523" class="Function">ℕ.*-comm</a> <a id="1553" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1532" class="Bound">m</a> <a id="1555" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1534" class="Bound">n</a> <a id="1557" class="Symbol">=</a> <a id="1559" href="Algebra.Properties.Monoid.Mult.TCOptimised.html#2363" class="Function">Mult.×-assocˡ</a> <a id="1573" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1530" class="Bound">x</a> <a id="1575" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1534" class="Bound">n</a> <a id="1577" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1532" class="Bound">m</a>
+<a id="1521" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1472" class="Function">^-assocʳ</a> <a id="1530" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1530" class="Bound">x</a> <a id="1532" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1532" class="Bound">m</a> <a id="1534" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1534" class="Bound">n</a> <a id="1536" class="Keyword">rewrite</a> <a id="1544" href="Data.Nat.Properties.html#22718" class="Function">ℕ.*-comm</a> <a id="1553" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1532" class="Bound">m</a> <a id="1555" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1534" class="Bound">n</a> <a id="1557" class="Symbol">=</a> <a id="1559" href="Algebra.Properties.Monoid.Mult.TCOptimised.html#2363" class="Function">Mult.×-assocˡ</a> <a id="1573" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1530" class="Bound">x</a> <a id="1575" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1534" class="Bound">n</a> <a id="1577" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1532" class="Bound">m</a>
 </pre></body></html>