From 67e152536feb0e6d3e3ef0f4286e019cf40e1dd0 Mon Sep 17 00:00:00 2001 From: Oscar11218 Date: Thu, 23 Oct 2025 11:41:06 -0400 Subject: [PATCH] Just trying --- Probability/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Probability/Basic.lean b/Probability/Basic.lean index f95efb3..5d075fa 100644 --- a/Probability/Basic.lean +++ b/Probability/Basic.lean @@ -41,7 +41,7 @@ abbrev Prob (p : ℚ) : Prop := 0 ≤ p ∧ p ≤ 1 namespace Prob -variable {p x y : ℚ} +variable {p x y : ℚ} --creating variables @[simp] theorem of_complement ( hp : Prob p) : Prob (1-p) := by