Theorems · Definition · linear algebra

Matrix.IsIrreducible.recOn

{n : Type u_1} →
  {R : Type u_2} →
    [inst : Ring R] →
      [inst_1 : LinearOrder R] →
        {A : Matrix n n R} →
          {motive : A.IsIrreducible → Sort u} →
            (t : A.IsIrreducible) →
              ((nonneg : ∀ (i j : n), 0 ≤ A i j) → (connected : Quiver.IsSStronglyConnected n) → motive ⋯) → motive t

Defined in: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Cited by: 0 results in Mathlib
Foundations: Depth 20 from the axioms · uses propext
Assumes: Ring LinearOrder

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites6

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
Matrix.IsIrreduciblestatement and proof · cited by 8
Quiver.IsSStronglyConnectedstatement and proof · cited by 8
Matrix.toQuiverstatement · cited by 6

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.