Auxiliary lemmas for Chapter 44 (Friendship Theorem)

Lemmas extracted from the main file that don't directly correspond to the tex blueprint.

Dedekind's lemma (1858): √m rational ⟹ √m integer

theorem chapter44.Nat.sqrt_rational_is_integer (m p q : ℕ) (hq : 0 < q) (hsq : p ^ 2 = m * q ^ 2) : q ∣ p

Dedekind's lemma (1858), infinite descent proof (the book's proof). If p² = m * q² with q > 0, then q ∣ p (and hence m is a perfect square).

theorem chapter44.Nat.sqrt_rational_is_integer_coprime (m p q : ℕ) (hq : 0 < q) (hcop : p.Coprime q) (hsq : p ^ 2 = m * q ^ 2) : q = 1

Dedekind's lemma (1858), alternative proof (coprime version).

Number-theoretic endgame

theorem chapter44.false_of_sq_mul_pred_eq_sq (d k : ℕ) (hd : 3 ≤ d) (hk : 0 < k) (heq : k ^ 2 * (d - 1) = d ^ 2) : False

Auxiliary lemmas for eigenvalue analysis

theorem chapter44.sq_sum_eq_sq_mul {ι : Type u_1} (S : Finset ι) (f : ι → ℝ) (c : ℕ) (hc : 0 < c) (hf : ∀ i ∈ S, f i ^ 2 = ↑c) : ∃ (k : ℕ), (∑ i ∈ S, f i) ^ 2 = ↑c * ↑k ^ 2

theorem chapter44.trace_unitary_conj {n : Type u_1} [Fintype n] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n ℝ)) (M : Matrix n n ℝ) : (((Unitary.conjStarAlgAut ℝ (Matrix n n ℝ)) U) M).trace = M.trace