have : (A ^ 2) = (k - 1) • (1 : Matrix V V R) + of (fun _ _ => 1) := by sorry
V : Type u
R : Type v
inst✝² : Semiring R
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : Nonempty V
h : ∀ ⦃v w : V⦄, v ≠ w → Fintype.card ↑(G.commonNeighbors v w) = 1
no_politician : ¬∃ v, ∀ (w : V), v ≠ w → G.Adj v w
lemma₁ : ∃ k, G.IsRegularOfDegree k
k : ℕ
hregular : G.IsRegularOfDegree k
n : ℕ := Fintype.card V
eq₁ : n = k ^ 2 - k + 1
this : 2 < k
A : Matrix V V R := adjMatrix R G
⊢ False
V : Type u
R : Type v
inst✝² : Semiring R
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : Nonempty V
h : ∀ ⦃v w : V⦄, v ≠ w → Fintype.card ↑(G.commonNeighbors v w) = 1
no_politician : ¬∃ v, ∀ (w : V), v ≠ w → G.Adj v w
lemma₁ : ∃ k, G.IsRegularOfDegree k
k : ℕ
hregular : G.IsRegularOfDegree k
n : ℕ := Fintype.card V
eq₁ : n = k ^ 2 - k + 1
this✝ : 2 < k
A : Matrix V V R := adjMatrix R G
this : A ^ 2 = (k - 1) • 1 + of fun x x => 1
⊢ False