From 925999959b3780493410b242796c46a714d2aaad Mon Sep 17 00:00:00 2001 From: "A. M. Berns" Date: Wed, 6 May 2026 05:48:43 -0400 Subject: [PATCH] Fix Perron-Frobenius index nonemptiness --- LeanEval/LinearAlgebra/PerronFrobenius.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/LeanEval/LinearAlgebra/PerronFrobenius.lean b/LeanEval/LinearAlgebra/PerronFrobenius.lean index 7118d6a..a592b83 100644 --- a/LeanEval/LinearAlgebra/PerronFrobenius.lean +++ b/LeanEval/LinearAlgebra/PerronFrobenius.lean @@ -13,11 +13,14 @@ A Perron-Frobenius style statement for irreducible nonnegative real matrices. Mathlib already exposes irreducibility of nonnegative matrices via `Matrix.IsIrreducible`, and spectral radius via `spectralRadius`. + +The `[Nonempty n]` assumption is necessary: for `n = Empty`, `Matrix.IsIrreducible` is vacuous, +but `Module.End.HasEigenvector` still requires a nonzero vector. -/ @[eval_problem] theorem irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius - {n : Type*} [Fintype n] [DecidableEq n] + {n : Type*} [Fintype n] [DecidableEq n] [Nonempty n] (A : Matrix n n ℝ) (hA : A.IsIrreducible) : ∃ v : n → ℝ,