lean_workbook_plus_82690

Proved

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

Let M be a symmetric matrix of order n such that $M^k=0$ for all k belongs to N. Show that M=0.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_82690 (n : ℕ) (M : Matrix (Fin n) (Fin n) ℝ) (hM : M.transpose = M) (hMk : ∀ k : ℕ, M ^ k = 0) : M = 0   :=  by sorry

Source