English
The permanent scales by a scalar: perm(c M) = c^{card(n)} perm(M).
Русский
Перманент масштабируется скалярно: perm(c M) = c^{|n|} perm(M).
LaTeX
$$$\\operatorname{permanent}(c \\cdot M) = c^{|n|} \\operatorname{permanent}(M)$$$
Lean4
@[simp]
theorem permanent_smul (M : Matrix n n R) (c : R) : permanent (c • M) = c ^ Fintype.card n * permanent M :=
by
simp only [permanent, smul_apply, smul_eq_mul, Finset.mul_sum]
congr
ext
rw [mul_comm]
conv in ∏ _, c * _ => simp [mul_comm c];
exact prod_mul_pow_card.symm