permanent_updateRow_smul — Mathlib

English

Updating a row by c·u scales the permanent by c: permanent(updateRow(M, j, c·u)) = c · permanent(updateRow(M, j, u)).

Русский

Обновление строки $j$ умножением на $c$ умножает перманент на $c$.

LaTeX

$$$\\operatorname{permanent}(\\text{updateRow}(M, j, c \\cdot u)) = c \\cdot \\operatorname{permanent}(\\text{updateRow}(M, j, u))$$$

Lean4

@[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, ← updateCol_transpose, permanent_updateCol_smul, updateCol_transpose, permanent_transpose]

Похожие утверждения