Theorems · Definition · linear algebra

doublyStochastic

(R : Type u_3) →
  (n : Type u_4) →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] →
        [inst_2 : Semiring R] → [inst_3 : PartialOrder R] → [IsOrderedRing R] → Submonoid (Matrix n n R)

A square matrix is doubly stochastic iff all entries are nonnegative, and left or right multiplication by the vector of all 1s gives the vector of all 1s.

Defined in

Mathlib.Analysis.Convex.DoublyStochasticMatrix

Cited by

22 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableEqSemiringPartialOrderIsOrderedRing