English
Updating a column by c·u scales the permanent by c: permanent(updateCol(M, j, c·u)) = c · permanent(updateCol(M, j, u)).
Русский
Обновление столбца \(j\) умножением на \(c\) умножает перманент на \(c\): perm(updateCol(M, j, c·u)) = c · perm(updateCol(M, j, u)).
LaTeX
$$$\\operatorname{permanent}(\\text{updateCol}(M, j, c \\cdot u)) = c \\cdot \\operatorname{permanent}(\\text{updateCol}(M, j, u))$$$
Lean4
@[simp]
theorem permanent_updateCol_smul (M : Matrix n n R) (j : n) (c : R) (u : n → R) :
permanent (updateCol M j <| c • u) = c * permanent (updateCol M j u) :=
by
simp only [permanent, ← mul_prod_erase _ _ (mem_univ j), updateCol_self, Pi.smul_apply, smul_eq_mul, mul_sum,
← mul_assoc]
congr 1 with p
rw [Finset.prod_congr rfl (fun i hi ↦ ?_)]
simp only [ne_eq, ne_of_mem_erase hi, not_false_eq_true, updateCol_ne]
