s

ErikEk · ErikEk · commit c18797e016b5 · 2025-10-20T16:25:10.000+07:00
diff --git a/theorems.lean b/theorems.lean
@@ -169,7 +169,6 @@ theorem and_imp_iff (P Q R : Prop) : (P ∧ Q → R) ↔ (P → Q → R) := by
     cases hpq with
     | intro hp hq => exact h hp hq
 
-
 /-
 example (p q r : Prop) : ((p ∨ q) → r) ↔ ((p → r) ∧ (q → r)) := by
     constructor
