def StochasticMatrix.toMatrix {M : ℕ} (P : StochasticMatrix M) : Matrix (Fin (M + 1)) (Fin (M + 1)) ℝ

Underlying matrix of probabilities of a StochasticMatrix.

def StochasticMatrix.IsErgodic {M : ℕ} (P : StochasticMatrix M) : Prop

A finite-state Markov chain (given by its stochastic transition matrix P) is ergodic if some positive power P^n has all strictly positive entries.