Theorems · Definition · linear algebra

Matrix.colStochastic

(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 column stochastic iff all entries are nonnegative, and left multiplication by the vector of all 1s gives the vector of all 1s.

Defined in

Mathlib.LinearAlgebra.Matrix.Stochastic

Cited by

19 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqSemiringPartialOrderIsOrderedRing