use permanent, which is now in mathlib

drive-by: clean up imports
mo271 · Nov 20, 2024 · 972688f · 972688f
1 parent cd57cbc
commit 972688f
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 12 deletions.
diff --git a/FormalBook/Chapter_02.lean b/FormalBook/Chapter_02.lean
@@ -3,14 +3,14 @@ Copyright 2022 Moritz Firsching. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Moritz Firsching
 -/
+import Mathlib.Algebra.Lie.OfAssociative
 import Mathlib.Analysis.Convex.SpecificFunctions.Basic
 import Mathlib.Analysis.Convex.SpecificFunctions.Deriv
 import Mathlib.Data.Nat.Choose.Factorization
 import Mathlib.Data.Real.StarOrdered
+import Mathlib.NumberTheory.Harmonic.Defs
 import Mathlib.NumberTheory.Primorial
 import Mathlib.Tactic.NormNum.Prime
-import Mathlib.NumberTheory.Harmonic.Defs
-import Mathlib
 /-!
 # Bertrand's postulate
 

diff --git a/FormalBook/Chapter_20.lean b/FormalBook/Chapter_20.lean
@@ -3,17 +3,13 @@ Copyright 2022 Moritz Firsching. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Moritz Firsching
 -/
+import FormalBook.Mathlib.EdgeFinset
 import Mathlib.Analysis.InnerProductSpace.Basic
 import Mathlib.Analysis.SpecialFunctions.Pow.Real
-import Mathlib.Data.Real.StarOrdered
-import Mathlib.Combinatorics.SimpleGraph.Basic
-import Mathlib.Combinatorics.SimpleGraph.Finite
+import Mathlib.Combinatorics.Enumerative.DoubleCounting
 import Mathlib.Combinatorics.SimpleGraph.Clique
 import Mathlib.Combinatorics.SimpleGraph.DegreeSum
-import Mathlib.Algebra.Order.BigOperators.Ring.Finset
-import FormalBook.Mathlib.EdgeFinset
-import Mathlib
-import Aesop
+import Mathlib.Data.Real.StarOrdered
 
 open Real
 open RealInnerProductSpace

diff --git a/FormalBook/Chapter_24.lean b/FormalBook/Chapter_24.lean
@@ -5,6 +5,7 @@ Authors: Moritz Firsching
 -/
 import Mathlib.Data.Matrix.DoublyStochastic
 import Mathlib.Data.Real.Basic
+import Mathlib.LinearAlgebra.Matrix.Permanent
 /-!
 # Van der Waerden's permanent conjecture
 
@@ -27,13 +28,11 @@ import Mathlib.Data.Real.Basic
 -/
 
 
-
 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
+    M ∈ doublyStochastic ℝ (Fin n) → permanent M ≥ (n.factorial)/(n ^ n) := sorry