theorem CompleteGraphSpectrum.lapMatrix_completeGraph_apply (n : ℕ) (i j : Fin n) : SimpleGraph.lapMatrix ℝ (SimpleGraph.completeGraph (Fin n)) i j = if i = j then ↑n - 1 else -1

theorem CompleteGraphSpectrum.lapMatrix_completeGraph_mulVec (n : ℕ) (v : Fin n → ℝ) : (SimpleGraph.lapMatrix ℝ (SimpleGraph.completeGraph (Fin n))).mulVec v = fun (i : Fin n) => ↑n * v i - ∑ j : Fin n, v j

noncomputable def CompleteGraphSpectrum.completeGraphLapEnd (n : ℕ) : Module.End ℝ (Fin n → ℝ)

noncomputable def CompleteGraphSpectrum.sumFunctional (n : ℕ) : (Fin n → ℝ) →ₗ[ℝ] ℝ

theorem CompleteGraphSpectrum.eigenspace_n_eq_ker_sumFunctional (n : ℕ) : (completeGraphLapEnd n).eigenspace ↑n = (sumFunctional n).ker

theorem CompleteGraphSpectrum.eigenspace_zero_eq_span_ones (n : ℕ) (hn : 1 ≤ n) : (completeGraphLapEnd n).eigenspace 0 = ℝ ∙ fun (x : Fin n) => 1

theorem CompleteGraphSpectrum.sumFunctional_surjective (n : ℕ) (hn : 1 ≤ n) : Function.Surjective ⇑(sumFunctional n)

theorem CompleteGraphSpectrum.finrank_eigenspace_n (n : ℕ) (hn : 1 ≤ n) : Module.finrank ℝ ↥((completeGraphLapEnd n).eigenspace ↑n) = n - 1

theorem CompleteGraphSpectrum.finrank_eigenspace_zero (n : ℕ) (hn : 1 ≤ n) : Module.finrank ℝ ↥((completeGraphLapEnd n).eigenspace 0) = 1

theorem CompleteGraphSpectrum.lemma15_complete_graph_spectrum (n : ℕ) (hn : 1 ≤ n) : Module.finrank ℝ ↥((completeGraphLapEnd n).eigenspace 0) = 1 ∧ ((completeGraphLapEnd n).eigenspace 0 = ℝ ∙ fun (x : Fin n) => 1) ∧ Module.finrank ℝ ↥((completeGraphLapEnd n).eigenspace ↑n) = n - 1 ∧ (completeGraphLapEnd n).eigenspace ↑n = (sumFunctional n).ker