From 0aabc1e0c6acff8f16c65ce47c068392e9eb961a Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Tue, 12 Nov 2024 11:05:48 +0100
Subject: [PATCH] add permanent conjecture

---
 FormalBook/Chapter_24.lean | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/FormalBook/Chapter_24.lean b/FormalBook/Chapter_24.lean
index 1224e42..38f5e56 100644
--- a/FormalBook/Chapter_24.lean
+++ b/FormalBook/Chapter_24.lean
@@ -15,7 +15,8 @@ limitations under the License.
 
 Authors: Moritz Firsching
 -/
-import Mathlib.Tactic
+import Mathlib.Data.Matrix.DoublyStochastic
+import Mathlib.Data.Real.Basic
 /-!
 # Van der Waerden's permanent conjecture
 
@@ -36,3 +37,15 @@ import Mathlib.Tactic
     - Claim
   - Farkas Lemma
 -/
+
+
+
+open Equiv
+namespace Matrix
+
+variable {n : ℕ}
+
+def per (M : Matrix (Fin n) (Fin n) ℝ) := ∑ σ : Perm (Fin n), ∏ i, M (σ i) i
+
+theorem permanent_conjecture (M : Matrix (Fin n) (Fin n) ℝ) :
+    M ∈ doublyStochastic ℝ (Fin n) →  per M ≥ (n.factorial)/(n ^ n) := sorry