From 18cf480be6c6592edbe236b95e40905bb84b1a22 Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Tue, 12 Nov 2024 11:19:01 +0100
Subject: [PATCH] add permanent conjecture (#75)

---
 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..717d909 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