From 4f571a36c89bfb519ac720451bc6facb88959331 Mon Sep 17 00:00:00 2001
From: Taksh <takshkothari09@gmail.com>
Date: Mon, 7 Sep 2026 17:37:43 +0530
Subject: [PATCH] Fill countable additivity of the zero measure.

---
 Analysis/MeasureTheory/Section_1_4_3.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Analysis/MeasureTheory/Section_1_4_3.lean b/Analysis/MeasureTheory/Section_1_4_3.lean
index 60d13f856..edf882679 100644
--- a/Analysis/MeasureTheory/Section_1_4_3.lean
+++ b/Analysis/MeasureTheory/Section_1_4_3.lean
@@ -197,7 +197,7 @@ noncomputable instance CountablyAdditiveMeasure.instZero {X:Type*} (B: ConcreteS
   {
     zero := {
       toFinitelyAdditiveMeasure := 0
-      measure_countable_additive := by sorry
+      measure_countable_additive := fun _ _ _ => tsum_zero.symm
     }
   }