lean_workbook_plus_291

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Let A be a matrix nXn with $a_{ij}\ge{0}$ for every i,j=1,2,...,n and $\sum_{j=1}^{n}a_{ij}=1$ for every i=1,2,..,n. Show that if a is an eigenvalue of A then $|a|\leq{1}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_291 (n : ℕ) (hn : 0 < n) (a : Matrix (Fin n) (Fin n) ℝ) (ha : ∀ i j, 0 ≤ a i j) (h : ∀ i, ∑ j, a i j = 1) (a_eig : ∃ v : Fin n → ℝ, ∃ l : ℝ, a.mulVec v = l • v) : ∃ v : Fin n → ℝ, ∃ l : ℝ, a.mulVec v = l • v ∧ l ≤ 1 ∧ -1 ≤ l   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph