Documentation Verification Report

Defs

📁 Source: Mathlib/LinearAlgebra/Matrix/Irreducible/Defs.lean

Statistics

Metric	Count
Definitions `IsIrreducible`, `IsPrimitive`, `toQuiver`, `transposePath`	4
Theorems `connected`, `exists_pos`, `nonneg`, `transpose`, `exists_pos_pow`, `isIrreducible`, `nonneg`, `isIrreducible_iff`, `isIrreducible_iff_exists_pow_pos`, `isIrreducible_transpose_iff`, `isPrimitive_iff`, `pow_apply_pos_iff_nonempty_path`	12
Total	16

Matrix

Definitions

Name	Category	Theorems
`IsIrreducible` 📖	CompData	4 math math: `isIrreducible_transpose_iff`, `IsPrimitive.isIrreducible`, `isIrreducible_iff_exists_pow_pos`, `isIrreducible_iff`
`IsPrimitive` 📖	CompData	1 math math: `isPrimitive_iff`
`toQuiver` 📖	CompOp	3 math math: `pow_apply_pos_iff_nonempty_path`, `isIrreducible_iff`, `IsIrreducible.connected`
`transposePath` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIrreducible_iff` 📖	mathematical	—	`IsIrreducible` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Quiver.IsSStronglyConnected` `toQuiver`	—	—
`isIrreducible_iff_exists_pow_pos` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`IsIrreducible` `Preorder.toLT` `Matrix` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `Ring.toSemiring`	—	`IsIrreducible.connected` `pow_apply_pos_iff_nonempty_path`
`isIrreducible_transpose_iff` 📖	mathematical	—	`IsIrreducible` `transpose`	—	`IsIrreducible.transpose` `isIrreducible_iff` `Nat.instCanonicallyOrderedAdd`
`isPrimitive_iff` 📖	mathematical	—	`IsPrimitive` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Preorder.toLT` `Matrix` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `Ring.toSemiring`	—	—
`pow_apply_pos_iff_nonempty_path` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Preorder.toLT` `Matrix` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `Ring.toSemiring` `Quiver.Path` `toQuiver` `Quiver.Path.length`	—	`eq_or_ne` `pow_zero` `one_apply_ne` `Quiver.Path.eq_of_length_zero` `one_apply_eq` `IsOrderedRing.toZeroLEOneClass` `NeZero.one` `pow_succ` `mul_apply` `Finset.sum_pos_iff_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `mul_nonneg` `IsOrderedRing.toPosMulMono` `pow_apply_nonneg` `le_antisymm` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `mul_pos` `Finset.mem_univ`

Matrix.IsIrreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`connected` 📖	mathematical	`Matrix.IsIrreducible`	`Quiver.IsSStronglyConnected` `Matrix.toQuiver`	—	—
`exists_pos` 📖	mathematical	`Matrix.IsIrreducible`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`exists_pair_ne` `connected` `Quiver.Path.exists_eq_comp_of_le_length` `Quiver.Path.length_ne_zero_iff_eq_cons` `Quiver.Path.eq_of_length_zero` `IsEmpty.false`
`nonneg` 📖	mathematical	`Matrix.IsIrreducible`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—
`transpose` 📖	mathematical	`Matrix.IsIrreducible`	`Matrix.transpose`	—	`nonneg` `connected` `Quiver.Path.length_comp` `Nat.instCanonicallyOrderedAdd` `Nat.instZeroLEOneClass`

Matrix.IsPrimitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_pos_pow` 📖	mathematical	`Matrix.IsPrimitive`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Matrix` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Ring.toSemiring`	—	—
`isIrreducible` 📖	mathematical	`Matrix.IsPrimitive`	`Matrix.IsIrreducible`	—	`Matrix.isIrreducible_iff_exists_pow_pos`
`nonneg` 📖	mathematical	`Matrix.IsPrimitive`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—

---

← Back to Index