Hadamard's conjecture

Exercise · isHadamard_equiv_isHadamard'

Both definitions are equivalent.

TODO(firsching): complete and golf the proof

Formal statement · Lean 4.lean

theorem isHadamard_equiv_isHadamard' (n : ℕ) (M : Matrix (Fin n) (Fin n) ℝ) : IsHadamard' M ↔ IsHadamard M := by
  sorry

Proof. sorry

Nobody has tried yet.