lean_workbook_plus_55463

Proved

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

Determine if there exists an integer $n > 0$ such that $A^n = I$ , where $A$ is a square matrix with 1s on the diagonal and 0s everywhere else, and $I$ is the identity matrix.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_55463 (n : ℕ) (hn : 0 < n) (A : Matrix (Fin n) (Fin n) ℤ) (hA : A.diag = 1 ∧ ∀ i j, i ≠ j → A i j = 0) : ∃ k : ℕ, A ^ k = 1   :=  by sorry

Source

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

View graph