Deploying to gh-pages from @ dfde0ac 🚀

Author: github-merge-queue[bot]

master/Algebra.Apartness.Properties.HeytingCommutativeRing.html

@@ -20,7 +20,7 @@
 <a id="686" class="Keyword">open</a> <a id="691" href="Algebra.Bundles.html#30337" class="Module">CommutativeRing</a> <a id="707" href="Algebra.Apartness.Bundles.html#1260" class="Function">commutativeRing</a> <a id="723" class="Keyword">using</a> <a id="729" class="Symbol">(</a><a id="730" href="Algebra.Bundles.html#30807" class="Function">ring</a><a id="734" class="Symbol">;</a> <a id="736" href="Algebra.Bundles.html#20484" class="Function">*-commutativeMonoid</a><a id="755" class="Symbol">)</a>
 
 <a id="758" class="Keyword">open</a> <a id="763" class="Keyword">import</a> <a id="770" href="Algebra.Properties.Ring.html" class="Module">Algebra.Properties.Ring</a> <a id="794" href="Algebra.Bundles.html#30807" class="Function">ring</a>
-  <a id="801" class="Keyword">using</a> <a id="807" class="Symbol">(</a><a id="808" href="Algebra.Properties.RingWithoutOne.html#749" class="Function">-0#≈0#</a><a id="814" class="Symbol">;</a> <a id="816" href="Algebra.Properties.RingWithoutOne.html#1218" class="Function">-‿distribˡ-*</a><a id="828" class="Symbol">;</a> <a id="830" href="Algebra.Properties.RingWithoutOne.html#1787" class="Function">-‿distribʳ-*</a><a id="842" class="Symbol">;</a> <a id="844" href="Algebra.Properties.RingWithoutOne.html#954" class="Function">-‿anti-homo-+</a><a id="857" class="Symbol">;</a> <a id="859" href="Algebra.Properties.RingWithoutOne.html#881" class="Function">-‿involutive</a><a id="871" class="Symbol">)</a>
+  <a id="801" class="Keyword">using</a> <a id="807" class="Symbol">(</a><a id="808" href="Algebra.Properties.RingWithoutOne.html#780" class="Function">-0#≈0#</a><a id="814" class="Symbol">;</a> <a id="816" href="Algebra.Properties.RingWithoutOne.html#1249" class="Function">-‿distribˡ-*</a><a id="828" class="Symbol">;</a> <a id="830" href="Algebra.Properties.RingWithoutOne.html#1818" class="Function">-‿distribʳ-*</a><a id="842" class="Symbol">;</a> <a id="844" href="Algebra.Properties.RingWithoutOne.html#985" class="Function">-‿anti-homo-+</a><a id="857" class="Symbol">;</a> <a id="859" href="Algebra.Properties.RingWithoutOne.html#912" class="Function">-‿involutive</a><a id="871" class="Symbol">)</a>
 <a id="873" class="Keyword">open</a> <a id="878" class="Keyword">import</a> <a id="885" href="Relation.Binary.Definitions.html" class="Module">Relation.Binary.Definitions</a> <a id="913" class="Keyword">using</a> <a id="919" class="Symbol">(</a><a id="920" href="Relation.Binary.Definitions.html#1491" class="Function">Symmetric</a><a id="929" class="Symbol">)</a>
 <a id="931" class="Keyword">import</a> <a id="938" href="Relation.Binary.Reasoning.Setoid.html" class="Module">Relation.Binary.Reasoning.Setoid</a> <a id="971" class="Symbol">as</a> <a id="974" class="Module">≈-Reasoning</a>
 <a id="986" class="Keyword">open</a> <a id="991" class="Keyword">import</a> <a id="998" href="Algebra.Properties.CommutativeMonoid.html" class="Module">Algebra.Properties.CommutativeMonoid</a> <a id="1035" href="Algebra.Bundles.html#20484" class="Function">*-commutativeMonoid</a>
@@ -29,13 +29,13 @@
   <a id="1075" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1075" class="Generalizable">x</a> <a id="1077" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1077" class="Generalizable">y</a> <a id="1079" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1079" class="Generalizable">z</a> <a id="1081" class="Symbol">:</a> <a id="1083" href="Algebra.Apartness.Bundles.html#779" class="Field">Carrier</a>
 
 <a id="invertibleˡ⇒#"></a><a id="1092" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1092" class="Function">invertibleˡ⇒#</a> <a id="1106" class="Symbol">:</a> <a id="1108" href="Algebra.Definitions.html#2495" class="Function">LeftInvertible</a> <a id="1123" href="Algebra.Apartness.Bundles.html#816" class="Field Operator">_≈_</a> <a id="1127" href="Algebra.Apartness.Bundles.html#1076" class="Field">1#</a> <a id="1130" href="Algebra.Apartness.Bundles.html#951" class="Field Operator">_*_</a> <a id="1134" class="Symbol">(</a><a id="1135" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1075" class="Generalizable">x</a> <a id="1137" href="Algebra.Structures.html#8953" class="Function Operator">-</a> <a id="1139" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1077" class="Generalizable">y</a><a id="1140" class="Symbol">)</a> <a id="1142" class="Symbol">→</a> <a id="1144" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1075" class="Generalizable">x</a> <a id="1146" href="Algebra.Apartness.Bundles.html#862" class="Field Operator">#</a> <a id="1148" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1077" class="Generalizable">y</a>
-<a id="1150" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1092" class="Function">invertibleˡ⇒#</a> <a id="1164" class="Symbol">=</a> <a id="1166" href="Algebra.Apartness.Structures.html#1478" class="Function">invertible⇒#</a> <a id="1179" href="Function.Base.html#1115" class="Function Operator">∘</a> <a id="1181" href="Algebra.Properties.CommutativeMonoid.html#1152" class="Function">invertibleˡ⇒invertible</a>
+<a id="1150" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1092" class="Function">invertibleˡ⇒#</a> <a id="1164" class="Symbol">=</a> <a id="1166" href="Algebra.Apartness.Structures.html#1478" class="Function">invertible⇒#</a> <a id="1179" href="Function.Base.html#1115" class="Function Operator">∘</a> <a id="1181" href="Algebra.Properties.CommutativeMonoid.html#1155" class="Function">invertibleˡ⇒invertible</a>
 
 <a id="invertibleʳ⇒#"></a><a id="1205" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1205" class="Function">invertibleʳ⇒#</a> <a id="1219" class="Symbol">:</a> <a id="1221" href="Algebra.Definitions.html#2583" class="Function">RightInvertible</a> <a id="1237" href="Algebra.Apartness.Bundles.html#816" class="Field Operator">_≈_</a> <a id="1241" href="Algebra.Apartness.Bundles.html#1076" class="Field">1#</a> <a id="1244" href="Algebra.Apartness.Bundles.html#951" class="Field Operator">_*_</a> <a id="1248" class="Symbol">(</a><a id="1249" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1075" class="Generalizable">x</a> <a id="1251" href="Algebra.Structures.html#8953" class="Function Operator">-</a> <a id="1253" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1077" class="Generalizable">y</a><a id="1254" class="Symbol">)</a> <a id="1256" class="Symbol">→</a> <a id="1258" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1075" class="Generalizable">x</a> <a id="1260" href="Algebra.Apartness.Bundles.html#862" class="Field Operator">#</a> <a id="1262" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1077" class="Generalizable">y</a>
-<a id="1264" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1205" class="Function">invertibleʳ⇒#</a> <a id="1278" class="Symbol">=</a> <a id="1280" href="Algebra.Apartness.Structures.html#1478" class="Function">invertible⇒#</a> <a id="1293" href="Function.Base.html#1115" class="Function Operator">∘</a> <a id="1295" href="Algebra.Properties.CommutativeMonoid.html#1326" class="Function">invertibleʳ⇒invertible</a>
+<a id="1264" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1205" class="Function">invertibleʳ⇒#</a> <a id="1278" class="Symbol">=</a> <a id="1280" href="Algebra.Apartness.Structures.html#1478" class="Function">invertible⇒#</a> <a id="1293" href="Function.Base.html#1115" class="Function Operator">∘</a> <a id="1295" href="Algebra.Properties.CommutativeMonoid.html#1329" class="Function">invertibleʳ⇒invertible</a>
 
 <a id="x-0≈x"></a><a id="1319" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1319" class="Function">x-0≈x</a> <a id="1325" class="Symbol">:</a> <a id="1327" href="Algebra.Definitions.html#1781" class="Function">RightIdentity</a> <a id="1341" href="Algebra.Apartness.Bundles.html#816" class="Field Operator">_≈_</a> <a id="1345" href="Algebra.Apartness.Bundles.html#1037" class="Field">0#</a> <a id="1348" href="Algebra.Structures.html#8953" class="Function Operator">_-_</a>
-<a id="1352" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1319" class="Function">x-0≈x</a> <a id="1358" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1358" class="Bound">x</a> <a id="1360" class="Symbol">=</a> <a id="1362" href="Relation.Binary.Structures.html#1648" class="Function">trans</a> <a id="1368" class="Symbol">(</a><a id="1369" href="Algebra.Structures.html#20045" class="Function">+-congˡ</a> <a id="1377" href="Algebra.Properties.RingWithoutOne.html#749" class="Function">-0#≈0#</a><a id="1383" class="Symbol">)</a> <a id="1385" class="Symbol">(</a><a id="1386" href="Algebra.Structures.html#20216" class="Function">+-identityʳ</a> <a id="1398" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1358" class="Bound">x</a><a id="1399" class="Symbol">)</a>
+<a id="1352" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1319" class="Function">x-0≈x</a> <a id="1358" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1358" class="Bound">x</a> <a id="1360" class="Symbol">=</a> <a id="1362" href="Relation.Binary.Structures.html#1648" class="Function">trans</a> <a id="1368" class="Symbol">(</a><a id="1369" href="Algebra.Structures.html#20045" class="Function">+-congˡ</a> <a id="1377" href="Algebra.Properties.RingWithoutOne.html#780" class="Function">-0#≈0#</a><a id="1383" class="Symbol">)</a> <a id="1385" class="Symbol">(</a><a id="1386" href="Algebra.Structures.html#20216" class="Function">+-identityʳ</a> <a id="1398" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1358" class="Bound">x</a><a id="1399" class="Symbol">)</a>
 
 <a id="1#0"></a><a id="1402" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1402" class="Function">1#0</a> <a id="1406" class="Symbol">:</a> <a id="1408" href="Algebra.Apartness.Bundles.html#1076" class="Field">1#</a> <a id="1411" href="Algebra.Apartness.Bundles.html#862" class="Field Operator">#</a> <a id="1413" href="Algebra.Apartness.Bundles.html#1037" class="Field">0#</a>
 <a id="1416" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1402" class="Function">1#0</a> <a id="1420" class="Symbol">=</a> <a id="1422" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1092" class="Function">invertibleˡ⇒#</a> <a id="1436" class="Symbol">(</a><a id="1437" href="Algebra.Apartness.Bundles.html#1076" class="Field">1#</a> <a id="1440" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="1442" href="Algebra.Apartness.Properties.HeytingCommutativeRing.html#1463" class="Function">1*[x-0]≈x</a><a id="1451" class="Symbol">)</a>

master/Algebra.Module.Properties.html

@@ -19,8 +19,8 @@
 
 <a id="556" class="Keyword">open</a> <a id="561" href="Algebra.Module.Bundles.html#11352" class="Module">Module</a> <a id="568" href="Algebra.Module.Properties.html#517" class="Bound">mod</a>
 <a id="572" class="Keyword">open</a> <a id="577" class="Keyword">import</a> <a id="584" href="Algebra.Module.Properties.Semimodule.html" class="Module">Algebra.Module.Properties.Semimodule</a> <a id="621" href="Algebra.Module.Bundles.html#12329" class="Function">semimodule</a> <a id="632" class="Keyword">public</a>
-<a id="639" class="Keyword">open</a> <a id="644" class="Keyword">import</a> <a id="651" href="Algebra.Properties.Group.html" class="Module">Algebra.Properties.Group</a> <a id="676" class="Keyword">using</a> <a id="682" class="Symbol">(</a><a id="683" href="Algebra.Properties.Group.html#3359" class="Function">⁻¹-involutive</a><a id="696" class="Symbol">)</a>
+<a id="639" class="Keyword">open</a> <a id="644" class="Keyword">import</a> <a id="651" href="Algebra.Properties.Group.html" class="Module">Algebra.Properties.Group</a> <a id="676" class="Keyword">using</a> <a id="682" class="Symbol">(</a><a id="683" href="Algebra.Properties.Group.html#3377" class="Function">⁻¹-involutive</a><a id="696" class="Symbol">)</a>
 
 <a id="-ᴹ-involutive"></a><a id="699" href="Algebra.Module.Properties.html#699" class="Function">-ᴹ-involutive</a> <a id="713" class="Symbol">:</a> <a id="715" href="Algebra.Definitions.html#4273" class="Function">Involutive</a> <a id="726" href="Algebra.Module.Bundles.html#11607" class="Field Operator">_≈ᴹ_</a> <a id="731" href="Algebra.Module.Bundles.html#11742" class="Field Operator">-ᴹ_</a>
-<a id="735" href="Algebra.Module.Properties.html#699" class="Function">-ᴹ-involutive</a> <a id="749" class="Symbol">=</a> <a id="751" href="Algebra.Properties.Group.html#3359" class="Function">⁻¹-involutive</a> <a id="765" href="Algebra.Module.Bundles.html#4277" class="Function">+ᴹ-group</a>
+<a id="735" href="Algebra.Module.Properties.html#699" class="Function">-ᴹ-involutive</a> <a id="749" class="Symbol">=</a> <a id="751" href="Algebra.Properties.Group.html#3377" class="Function">⁻¹-involutive</a> <a id="765" href="Algebra.Module.Bundles.html#4277" class="Function">+ᴹ-group</a>
 </pre></body></html>