Theorems · Definition · linear algebra

Matrix.rowStochastic

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

Defined in

Mathlib.LinearAlgebra.Matrix.Stochastic

Cited by

18 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqSemiringPartialOrderIsOrderedRing