Square_of_Ones_Matrix
Provedlinear-algebramatricesproofwiki
The square of the n x n ones matrix J satisfies J^2 = nJ.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.LinearAlgebra.Matrix.Adjugate
Formal statement
theorem Square_of_Ones_Matrix (n : ℕ) (J : Matrix (Fin n) (Fin n) ℕ) (hJ : ∀ i j, J i j = 1) : ∀ i j, (J * J) i j = n := by sorry
Source