Theorems · Theorem · linear algebra

Matrix.pow_apply_pos_iff_nonempty_path

∀ {n : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] {A : Matrix n n R} [inst_2 : Fintype n]
  [IsOrderedRing R] [PosMulStrictMono R] [Nontrivial R] [inst_6 : DecidableEq n],
  (∀ (i j : n), 0 ≤ A i j) → ∀ (k : ℕ) (i j : n), 0 < (A ^ k) i j ↔ Nonempty { p // p.length = k }

For a matrix A with nonnegative entries, the (i, j)-entry of the k-th power A ^ k is strictly positive if and only if there exists a path of length k from i to j in the quiver associated to A via toQuiver.

Defined in

Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingLinearOrderFintypeIsOrderedRingPosMulStrictMonoNontrivialDecidableEq