Theorems · Theorem · combinatorics

Matrix.IsHadamard.card_eq_mul_star_of_const_col_sum

∀ {n : Type u_2} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R] [inst_3 : StarRing R]
  {A : Matrix n n R} {s : R},
  A.IsHadamard → IsRegular ↑(Fintype.card n) → (∀ (j : n), ∑ i, A i j = s) → ↑(Fintype.card n) = s * star s

A Hadamard matrix with constant column sum s has order s * star s, provided the order is regular in R. The row-sum form is IsHadamard.card_eq_star_mul_of_const_row_sum; over a ring with trivial star the conclusion becomes (Fintype.card n : R) = s ^ 2, a slightly stronger form of [Theorem 2.3.7][deLauneyFlannery2011]: only a constant sum hypothesis on one side is needed under the two-sided orthogonality condition.

Defined in

Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Cited by

1 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableEqSemiringStarRing