Commutative semiring of formal power series on commutative semirings

src/commutative-algebra.lagda.md

@@ -16,6 +16,8 @@ open import commutative-algebra.dependent-products-commutative-semirings public
 open import commutative-algebra.discrete-fields public
 open import commutative-algebra.eisenstein-integers public
 open import commutative-algebra.euclidean-domains public
+open import commutative-algebra.formal-power-series-commutative-rings public
+open import commutative-algebra.formal-power-series-commutative-semirings public
 open import commutative-algebra.full-ideals-commutative-rings public
 open import commutative-algebra.function-commutative-rings public
 open import commutative-algebra.function-commutative-semirings public

src/commutative-algebra/commutative-rings.lagda.md

@@ -318,6 +318,10 @@ module _
     add-Commutative-Ring (neg-Commutative-Ring x) (neg-Commutative-Ring y)
   distributive-neg-add-Commutative-Ring =
     distributive-neg-add-Ab ab-Commutative-Ring
+
+  neg-zero-Commutative-Ring :
+    neg-Commutative-Ring zero-Commutative-Ring ＝ zero-Commutative-Ring
+  neg-zero-Commutative-Ring = neg-zero-Ring ring-Commutative-Ring
 ```
 
 ### Multiplication in a commutative ring

src/commutative-algebra/commutative-semirings.lagda.md

@@ -10,6 +10,7 @@ module commutative-algebra.commutative-semirings where
 open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.natural-numbers
 
+open import foundation.action-on-identifications-binary-functions
 open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.iterated-dependent-product-types
@@ -176,6 +177,11 @@ module _
     (x y : type-Commutative-Semiring) → type-Commutative-Semiring
   mul-Commutative-Semiring' = mul-Semiring' semiring-Commutative-Semiring
 
+  ap-mul-Commutative-Semiring :
+    {x x' y y' : type-Commutative-Semiring} (p : Id x x') (q : Id y y') →
+    Id (mul-Commutative-Semiring x y) (mul-Commutative-Semiring x' y')
+  ap-mul-Commutative-Semiring p q = ap-binary mul-Commutative-Semiring p q
+
   one-Commutative-Semiring : type-Commutative-Semiring
   one-Commutative-Semiring = one-Semiring semiring-Commutative-Semiring