lean_workbook_plus_58975

Proved

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

Express the matrix $X$ as a 2x2 matrix with variables a, b, c, and d.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_58975 (X : Matrix (Fin 2) (Fin 2) ℝ) : ∃ a b c d : ℝ, X =!![a, b; c, d]   :=  by sorry

Source