sum_row_of_mem_doublyStochastic — Mathlib

English

For a doubly stochastic matrix, every row sums to 1.

Русский

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

LaTeX

$$$M\in doublyStochastic(R,n)\Rightarrow \sum_j M_{ij}=1\quad\text{for all } i.$$$

Lean4

/-- Each row sum of a doubly stochastic matrix is 1. -/
theorem sum_row_of_mem_doublyStochastic (hM : M ∈ doublyStochastic R n) (i : n) : ∑ j, M i j = 1 :=
  (mem_doublyStochastic_iff_sum.1 hM).2.1 _

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