From 0d8b4581bdd45743df25c91926711e5b1213ea7c Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Thu, 15 Feb 2024 16:01:24 +0100
Subject: [PATCH] fix layout

---
 Cubical/Algebra/CommRing/Localisation/Limit.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cubical/Algebra/CommRing/Localisation/Limit.agda b/Cubical/Algebra/CommRing/Localisation/Limit.agda
index afd060cb27..6f65e200ac 100644
--- a/Cubical/Algebra/CommRing/Localisation/Limit.agda
+++ b/Cubical/Algebra/CommRing/Localisation/Limit.agda
@@ -155,7 +155,7 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') n) where
                                                                   (f i ^ l) x)) ⟩
         ∑ (λ i → α i · (f i ^ l · x))       ≡⟨ ∑Ext (λ i → cong (α i ·_) (fˡx≡0 i)) ⟩
         ∑ (λ i → α i · 0r)                  ≡⟨ ∑Ext (λ i → 0RightAnnihilates (α i)) ⟩
-        ∑ (replicateFinVec n 0r)      ≡⟨ ∑0r n ⟩
+        ∑ (replicateFinVec n 0r)            ≡⟨ ∑0r n ⟩
         0r ∎