permMatrix_mem_doublyStochastic — Mathlib

English

Permutation matrices are doubly stochastic.

Русский

Перестановочные матрицы являются двойно стохастическими.

LaTeX

$$$\sigma \in \mathrm{Equiv.Perm}(n) \Rightarrow \sigma\.permMatrix(R) \in \mathrm{doublyStochastic}(R,n)$$$

Lean4

/-- Any permutation matrix is doubly stochastic. -/
theorem permMatrix_mem_doublyStochastic {σ : Equiv.Perm n} : σ.permMatrix R ∈ doublyStochastic R n :=
  by
  rw [mem_doublyStochastic_iff_sum]
  refine ⟨fun i j => ?g1, ?g2, ?g3⟩
  case g1 => aesop
  case g2 => simp [Equiv.toPEquiv_apply]
  case g3 => simp [Equiv.toPEquiv_apply, ← Equiv.eq_symm_apply]

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