sum_col_of_mem_doublyStochastic — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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