Minor fixes

Author: Taneb

src/Algebra/Construct/Quotient/Ring/Properties/ChineseRemainderTheorem.agda

@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
--- The Chinese Remainder Theorem for arbitrary rings
---
 -- The Agda standard library
+--
+-- The Chinese Remainder Theorem for arbitrary rings
 ------------------------------------------------------------------------
 
 {-# OPTIONS --safe --cubical-compatible #-}

src/Algebra/Ideal.agda

@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
--- Ideals of a ring
---
 -- The Agda standard library
+--
+-- Ideals of a ring
 ------------------------------------------------------------------------
 
 {-# OPTIONS --safe --cubical-compatible #-}

src/Algebra/Ideal/Construct/Intersection.agda

@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
--- Intersection of ideals
---
 -- The Agda standard library
+--
+-- Intersection of ideals
 ------------------------------------------------------------------------
 
 {-# OPTIONS --safe --cubical-compatible #-}

src/Algebra/Ideal/Construct/Kernel.agda

@@ -1,4 +1,10 @@
-{-# OPTIONS --safe --without-K #-}
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The kernel of a ring homomorphism is an ideal
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --cubical-compatible #-}
 
 open import Algebra.Bundles
 open import Algebra.Morphism.Structures

src/Algebra/Ideal/Coprimality.agda

@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
--- Coprimality of ideals
---
 -- The Agda standard library
+--
+-- Coprimality of ideals
 ------------------------------------------------------------------------
 
 {-# OPTIONS --safe --cubical-compatible #-}

src/Algebra/NormalSubgroup/Construct/Intersection.agda

@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
--- Intersection of normal subgroups
---
 -- The Agda standard library
+--
+-- Intersection of normal subgroups
 ------------------------------------------------------------------------
 
 {-# OPTIONS --safe --cubical-compatible #-}
@@ -84,5 +84,3 @@ N ∩ M = record
   where
     module N = NormalSubgroup N
     module M = NormalSubgroup M
-
-

src/Algebra/NormalSubgroup/Construct/Kernel.agda

@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
--- The kernel of a group homomorphism is a normal subgroup
---
 -- The Agda standard library
+--
+-- The kernel of a group homomorphism is a normal subgroup
 ------------------------------------------------------------------------
 
 {-# OPTIONS --safe --cubical-compatible #-}
@@ -52,7 +52,7 @@ x ∙ₖ y = record
    { element = G.ε
    ; inKernel = ρ.ε-homo
    }
-     
+
 _⁻¹ₖ : Kernel → Kernel
 x ⁻¹ₖ = record
   { element = X.element G.⁻¹