one_vecMul_of_mem_doublyStochastic

English

The all-ones row vector times the matrix M equals the all-ones row vector.

Русский

Строка единиц слева умножает на матрицу M и получается провектор единиц слева.

LaTeX

$$$\mathbf{1}^T M = \mathbf{1}^T \;\text{ for } M\in doublyStochastic(R,n).$$$

Lean4

/-- The all-ones row vector multiplied with a doubly stochastic matrix is 1. -/
theorem one_vecMul_of_mem_doublyStochastic (hM : M ∈ doublyStochastic R n) : 1 ᵥ* M = 1 :=
  (mem_doublyStochastic.1 hM).2.2

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