swap to make the build work

leanprover-community · Nov 29, 2024 · 3751be7 · 3751be7
1 parent 7da4dd8
commit 3751be7
Showing 1 changed file with 6 additions and 6 deletions.
diff --git a/Mathlib/LinearAlgebra/Matrix/Permanent.lean b/Mathlib/LinearAlgebra/Matrix/Permanent.lean
@@ -92,12 +92,6 @@ theorem permanent_smul (M : Matrix n n R) (c : R) :
   conv in ∏ _ , c * _ => simp [mul_comm c];
   exact prod_mul_pow_card.symm
 
-@[simp]
-theorem permanent_updateRow_smul (M : Matrix n n R) (j : n) (c : R) (u : n → R) :
-    permanent (updateRow M j <| c • u) = c * permanent (updateRow M j u) := by
-  rw [← permanent_transpose, ← updateColumn_transpose, permanent_updateColumn_smul,
-    updateColumn_transpose, permanent_transpose]
-
 @[simp]
 theorem permanent_updateColumn_smul (M : Matrix n n R) (j : n) (c : R) (u : n → R) :
     permanent (updateColumn M j <| c • u) = c * permanent (updateColumn M j u) := by
@@ -107,4 +101,10 @@ theorem permanent_updateColumn_smul (M : Matrix n n R) (j : n) (c : R) (u : n
   rw [Finset.prod_congr rfl (fun i hi ↦ ?_)]
   simp only [ne_eq, ne_of_mem_erase hi, not_false_eq_true, updateColumn_ne]
 
+@[simp]
+theorem permanent_updateRow_smul (M : Matrix n n R) (j : n) (c : R) (u : n → R) :
+    permanent (updateRow M j <| c • u) = c * permanent (updateRow M j u) := by
+  rw [← permanent_transpose, ← updateColumn_transpose, permanent_updateColumn_smul,
+    updateColumn_transpose, permanent_transpose]
+
 end Matrix