Mathlib Map

Theorems · Definition · linear algebra

Matrix.toQuiver

{n : Type u_1} → {R : Type u_2} → [Ring R] → [LinearOrder R] → Matrix n n R → Quiver n

The directed graph (quiver) associated with a matrix A, with an edge i ⟶ j iff 0 < A i j.

Defined in
Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Cited by
6 results in Mathlib
Foundations
Depth 17 from the axioms · uses propext
Assumes
RingLinearOrder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Matrix.IsIrreducible.connected · cited by 3IsIrreducible.connectedMatrix.IsIrreducible.transpose · cited by 1IsIrreducible.transposeMatrix.isIrreducible_iff · cited by 1Matrix.isIrreducible_iffMatrix.isIrreducible_iff_exists_pow_pos · cited by 1Matrix.isIrreducible_iff_…Matrix.IsIrreducible.casesOn · cited by 1IsIrreducible.casesOnMatrix.pow_apply_pos_iff_nonempty_path · cited by 1Matrix.pow_apply_pos_iff_…Matrix.transposePath · cited by 1Matrix.transposePathMatrix.IsIrreducible.exists_pos · cited by 0IsIrreducible.exists_posMatrix.IsIrreducible.recOn · cited by 0IsIrreducible.recOnLinearOrder · cited by 8572LinearOrderRing · cited by 7463RingMatrix · cited by 4303MatrixQuiver · cited by 405QuiverMatrix.toQuiverCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • LinearOrderstatement and proof · cited by 8,572
  • Ringstatement and proof · cited by 7,463
  • Matrixstatement and proof · cited by 4,303
  • Quiverstatement · cited by 405

Cited by9

Results whose statement or proof uses this declaration.