Product_of_the_Incidence_Matrix_of_a_BIBD_with_its_Transpose
Provedblock-designscombinatoricsproofwiki
For any BIBD with parameters , let be its block incidence matrix. Then where * is * is the transpose of * is the all 's matrix * is the identity matrix. That is
Preamble
import Mathlib.Data.Matrix.Basic import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Formal statement
theorem Product_of_the_Incidence_Matrix_of_a_BIBD_with_its_Transpose {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) (r l : ℤ) (h : A * A.transpose = (r - l) • (1 : Matrix (Fin n) (Fin n) ℤ) + l • Matrix.of (fun _ _ => (1 : ℤ))) : True := by sorrySource