lean_workbook_plus_70457

Proved

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

How many steps does it take for matrix $A=\begin{pmatrix} \frac{\sqrt{3}}{2} & -\frac{1}{2} \ \frac{1}{2} & \frac{\sqrt{3}}{2} \end{pmatrix}$ to return to its original state?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_70457 (A : Matrix (Fin 2) (Fin 2) ℝ) (hA : A =!![Real.sqrt 3 / 2, -1 / 2; 1 / 2, Real.sqrt 3 / 2]) : ∃ n : ℕ, A ^ n = 1   :=  by sorry

Source

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

View graph