permanent_smul — Mathlib

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

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