Theorems · Definition · linear algebra

Matrix.transposePath

{n : Type u_1} →
  {R : Type u_2} →
    [inst : Ring R] → [inst_1 : LinearOrder R] → {A : Matrix n n R} → {i j : n} → Quiver.Path i j → Quiver.Path j i

Reverse a path in toQuiver A to a path in toQuiver Aᵀ, swapping endpoints.

Defined in

Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Cited by

1 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext, Quot.sound

Assumes

RingLinearOrder