Update LeanCamCombi/ProbLYM.lean

ctchou · YaelDillies · web-flow · commit 7820cf46431d · 2025-02-13T18:15:08.000-08:00
Co-authored-by: Yaël Dillies &lt;yael.dillies@gmail.com&gt;
diff --git a/LeanCamCombi/ProbLYM.lean b/LeanCamCombi/ProbLYM.lean
@@ -8,9 +8,9 @@ import Mathlib.Data.Fintype.Perm
 import Mathlib.Probability.UniformOn
 
 /-!
-# Proof of the LYM inequality using probability theory
+# The LYM inequality using probability theory
 
-This file contains a formalization of the proof of the LYM inequality using
+This file proves the LYM inequality using
 (very elementary) probability theory given in Section 1.2 of Prof. Yufei Zhao's
 lecture notes for MIT 18.226:
 
