mulVec_one_of_mem_doublyStochastic

English

A doubly stochastic matrix times the all-ones column vector equals the all-ones vector.

Русский

Двойственно стохастическая матрица умножается на столбец единиц и получается столбец единиц.

LaTeX

$$$M\in doublyStochastic(R,n)\Rightarrow M\mathbf{1}=\mathbf{1}.$$$

Lean4

/-- A doubly stochastic matrix multiplied with the all-ones column vector is 1. -/
theorem mulVec_one_of_mem_doublyStochastic (hM : M ∈ doublyStochastic R n) : M *ᵥ 1 = 1 :=
  (mem_doublyStochastic.1 hM).2.1

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