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 → ℝ,