Theorem: chapter07.Theorem₂ (FormalBook/Chapter_07.lean)

State before:
n : ℕ
⊢ ∃ M, (∀ (i j : Fin n), M i j = -1 ∨ M i j = 1) ∧ ↑M.det > (↑n.factorial).sqrt
Tactic:
sorry
State after:
no goals