From 9f0b5c03bff776a3da78ca9d020e0211dfbfbc04 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Tue, 12 Nov 2024 13:31:13 +0100 Subject: [PATCH] Permanent conjecture (#76) * add lean statement --- blueprint/lean_decls | 1 + blueprint/src/chapter/chapter24.tex | 1 + 2 files changed, 2 insertions(+) diff --git a/blueprint/lean_decls b/blueprint/lean_decls index cfe5764..99b1eed 100644 --- 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 index 1fb6c60..922a773 100644 --- 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}\]