requested changes

agda · Mar 7, 2022 · 131128e · 131128e
1 parent 7fdfb6c
commit 131128e
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/Cubical/Algebra/Polynomials.agda b/Cubical/Algebra/Polynomials.agda
@@ -758,3 +758,9 @@ module PolyMod (R' : CommRing ℓ) where
                                                                            ⟩
                  ((((a ∷ p) Poly* q) Poly* r)) ∎)
                (λ x y i q r  → isSetPoly _ _ (x q r) (y q r) i)
+
+
+
+----------------------------------------------------------------------------------------------
+-- An instantiation of Polynomials as a commutative ring can be found in CommRing/Instances --
+----------------------------------------------------------------------------------------------