Permanent conjecture (#76)

* add lean statement
mo271 · Nov 12, 2024 · 9f0b5c0 · 9f0b5c0
1 parent 18cf480
commit 9f0b5c0
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 0 deletions.
diff --git a/blueprint/lean_decls b/blueprint/lean_decls
@@ -44,6 +44,7 @@ harmonic_geometric_arithmetic₂
 harmonic_geometric_arithmetic₃
 mantel
 fundamental_theorem_of_algebra
+Matrix.permanent_conjecture
 chapter28.pigeon_hole_principle
 chapter28.handshaking
 chapter44.friendship_theorem

diff --git a/blueprint/src/chapter/chapter24.tex b/blueprint/src/chapter/chapter24.tex
@@ -2,6 +2,7 @@ \chapter{Van der Waerden's permanent conjecture}
 
 \begin{theorem}
   \label{vanderwaerden}
+  \lean{Matrix.permanent_conjecture}
   Let $M = (m_{ij})$ be a doubly stochastic $n \times n$ matrix.
   Then
   \[\per M \ge \frac{n!}{n^n}\]