Skip to content

Commit

Permalink
Deploying to gh-pages from @ 4f73645 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@felixwellen
felixwellen committed Feb 7, 2024
1 parent 19eced6 commit 296dbad
Show file tree
Hide file tree
Showing 68 changed files with 9,780 additions and 10,057 deletions.
6 changes: 3 additions & 3 deletions Cubical.Algebra.CommAlgebra.FGIdeal.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,9 +11,9 @@

<a id="289" class="Keyword">open</a> <a id="294" class="Keyword">import</a> <a id="301" href="Cubical.Algebra.CommRing.html" class="Module">Cubical.Algebra.CommRing</a>
<a id="326" class="Keyword">open</a> <a id="331" class="Keyword">import</a> <a id="338" href="Cubical.Algebra.CommRing.FGIdeal.html" class="Module">Cubical.Algebra.CommRing.FGIdeal</a> <a id="371" class="Keyword">using</a> <a id="377" class="Symbol">()</a>
<a id="392" class="Keyword">renaming</a> <a id="401" class="Symbol">(</a><a id="402" href="Cubical.Algebra.CommRing.FGIdeal.html#4028" class="Function">generatedIdeal</a> <a id="417" class="Symbol">to</a> <a id="420" class="Function">generatedIdealCommRing</a><a id="442" class="Symbol">;</a>
<a id="466" href="Cubical.Algebra.CommRing.FGIdeal.html#9264" class="Function">indInIdeal</a> <a id="477" class="Symbol">to</a> <a id="480" class="Function">ringIncInIdeal</a><a id="494" class="Symbol">;</a>
<a id="518" href="Cubical.Algebra.CommRing.FGIdeal.html#10241" class="Function">0FGIdeal</a> <a id="527" class="Symbol">to</a> <a id="530" class="Function">0FGIdealCommRing</a><a id="546" class="Symbol">)</a>
<a id="392" class="Keyword">renaming</a> <a id="401" class="Symbol">(</a><a id="402" href="Cubical.Algebra.CommRing.FGIdeal.html#4017" class="Function">generatedIdeal</a> <a id="417" class="Symbol">to</a> <a id="420" class="Function">generatedIdealCommRing</a><a id="442" class="Symbol">;</a>
<a id="466" href="Cubical.Algebra.CommRing.FGIdeal.html#9253" class="Function">indInIdeal</a> <a id="477" class="Symbol">to</a> <a id="480" class="Function">ringIncInIdeal</a><a id="494" class="Symbol">;</a>
<a id="518" href="Cubical.Algebra.CommRing.FGIdeal.html#10235" class="Function">0FGIdeal</a> <a id="527" class="Symbol">to</a> <a id="530" class="Function">0FGIdealCommRing</a><a id="546" class="Symbol">)</a>
<a id="548" class="Keyword">open</a> <a id="553" class="Keyword">import</a> <a id="560" href="Cubical.Algebra.CommAlgebra.html" class="Module">Cubical.Algebra.CommAlgebra</a>
<a id="588" class="Keyword">open</a> <a id="593" class="Keyword">import</a> <a id="600" href="Cubical.Algebra.CommAlgebra.Ideal.html" class="Module">Cubical.Algebra.CommAlgebra.Ideal</a>

Expand Down
18 changes: 9 additions & 9 deletions Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html
View file

Large diffs are not rendered by default.

20 changes: 10 additions & 10 deletions Cubical.Algebra.CommAlgebra.FPAlgebra.Instances.html
View file

Large diffs are not rendered by default.

8 changes: 4 additions & 4 deletions Cubical.Algebra.CommAlgebra.Ideal.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,8 @@
<a id="151" class="Keyword">open</a> <a id="156" class="Keyword">import</a> <a id="163" href="Cubical.Foundations.Powerset.html" class="Module">Cubical.Foundations.Powerset</a>

<a id="193" class="Keyword">open</a> <a id="198" class="Keyword">import</a> <a id="205" href="Cubical.Algebra.CommRing.html" class="Module">Cubical.Algebra.CommRing</a>
<a id="230" class="Keyword">open</a> <a id="235" class="Keyword">import</a> <a id="242" href="Cubical.Algebra.CommRing.Ideal.html" class="Module">Cubical.Algebra.CommRing.Ideal</a> <a id="273" class="Keyword">renaming</a> <a id="282" class="Symbol">(</a><a id="283" href="Cubical.Algebra.CommRing.Ideal.Base.html#3755" class="Function">IdealsIn</a> <a id="292" class="Symbol">to</a> <a id="295" class="Function">IdealsInCommRing</a><a id="311" class="Symbol">;</a>
<a id="366" href="Cubical.Algebra.CommRing.Ideal.Base.html#3942" class="Function">makeIdeal</a> <a id="376" class="Symbol">to</a> <a id="379" class="Function">makeIdealCommRing</a><a id="396" class="Symbol">)</a>
<a id="230" class="Keyword">open</a> <a id="235" class="Keyword">import</a> <a id="242" href="Cubical.Algebra.CommRing.Ideal.html" class="Module">Cubical.Algebra.CommRing.Ideal</a> <a id="273" class="Keyword">renaming</a> <a id="282" class="Symbol">(</a><a id="283" href="Cubical.Algebra.CommRing.Ideal.Base.html#3666" class="Function">IdealsIn</a> <a id="292" class="Symbol">to</a> <a id="295" class="Function">IdealsInCommRing</a><a id="311" class="Symbol">;</a>
<a id="366" href="Cubical.Algebra.CommRing.Ideal.Base.html#3853" class="Function">makeIdeal</a> <a id="376" class="Symbol">to</a> <a id="379" class="Function">makeIdealCommRing</a><a id="396" class="Symbol">)</a>
<a id="398" class="Keyword">open</a> <a id="403" class="Keyword">import</a> <a id="410" href="Cubical.Algebra.CommAlgebra.html" class="Module">Cubical.Algebra.CommAlgebra</a>
<a id="438" class="Keyword">open</a> <a id="443" class="Keyword">import</a> <a id="450" href="Cubical.Algebra.Ring.html" class="Module">Cubical.Algebra.Ring</a>

Expand All @@ -31,8 +31,8 @@
<a id="949" href="Cubical.Algebra.CommAlgebra.Ideal.html#700" class="Function">makeIdeal</a> <a id="959" class="Symbol">=</a> <a id="961" href="Cubical.Algebra.CommAlgebra.Ideal.html#379" class="Function">makeIdealCommRing</a> <a id="979" class="Symbol">{</a><a id="980" class="Argument">R</a> <a id="982" class="Symbol">=</a> <a id="984" href="Cubical.Algebra.CommAlgebra.Base.html#2233" class="Function">CommAlgebra→CommRing</a> <a id="1005" href="Cubical.Algebra.CommAlgebra.Ideal.html#564" class="Bound">A</a><a id="1006" class="Symbol">}</a>

<a id="1011" href="Cubical.Algebra.CommAlgebra.Ideal.html#1011" class="Function">0Ideal</a> <a id="1018" class="Symbol">:</a> <a id="1020" href="Cubical.Algebra.CommAlgebra.Ideal.html#593" class="Function">IdealsIn</a>
<a id="1031" href="Cubical.Algebra.CommAlgebra.Ideal.html#1011" class="Function">0Ideal</a> <a id="1038" class="Symbol">=</a> <a id="1040" href="Cubical.Algebra.CommRing.Ideal.Base.html#3215" class="Function">CommIdeal.0Ideal</a> <a id="1057" class="Symbol">(</a><a id="1058" href="Cubical.Algebra.CommAlgebra.Base.html#2233" class="Function">CommAlgebra→CommRing</a> <a id="1079" href="Cubical.Algebra.CommAlgebra.Ideal.html#564" class="Bound">A</a><a id="1080" class="Symbol">)</a>
<a id="1031" href="Cubical.Algebra.CommAlgebra.Ideal.html#1011" class="Function">0Ideal</a> <a id="1038" class="Symbol">=</a> <a id="1040" href="Cubical.Algebra.CommRing.Ideal.Base.html#3126" class="Function">CommIdeal.0Ideal</a> <a id="1057" class="Symbol">(</a><a id="1058" href="Cubical.Algebra.CommAlgebra.Base.html#2233" class="Function">CommAlgebra→CommRing</a> <a id="1079" href="Cubical.Algebra.CommAlgebra.Ideal.html#564" class="Bound">A</a><a id="1080" class="Symbol">)</a>

<a id="1085" href="Cubical.Algebra.CommAlgebra.Ideal.html#1085" class="Function">1Ideal</a> <a id="1092" class="Symbol">:</a> <a id="1094" href="Cubical.Algebra.CommAlgebra.Ideal.html#593" class="Function">IdealsIn</a>
<a id="1105" href="Cubical.Algebra.CommAlgebra.Ideal.html#1085" class="Function">1Ideal</a> <a id="1112" class="Symbol">=</a> <a id="1114" href="Cubical.Algebra.CommRing.Ideal.Base.html#3434" class="Function">CommIdeal.1Ideal</a> <a id="1131" class="Symbol">(</a><a id="1132" href="Cubical.Algebra.CommAlgebra.Base.html#2233" class="Function">CommAlgebra→CommRing</a> <a id="1153" href="Cubical.Algebra.CommAlgebra.Ideal.html#564" class="Bound">A</a><a id="1154" class="Symbol">)</a>
<a id="1105" href="Cubical.Algebra.CommAlgebra.Ideal.html#1085" class="Function">1Ideal</a> <a id="1112" class="Symbol">=</a> <a id="1114" href="Cubical.Algebra.CommRing.Ideal.Base.html#3345" class="Function">CommIdeal.1Ideal</a> <a id="1131" class="Symbol">(</a><a id="1132" href="Cubical.Algebra.CommAlgebra.Base.html#2233" class="Function">CommAlgebra→CommRing</a> <a id="1153" href="Cubical.Algebra.CommAlgebra.Ideal.html#564" class="Bound">A</a><a id="1154" class="Symbol">)</a>
</pre></body></html>
Loading

0 comments on commit 296dbad

Please sign in to comment.