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	5 math math: IsIrreducible.transpose, 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Matrix Monoid.toPow 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.toPow 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Matrix Monoid.toPow 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.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.toPow 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