@[implicit_reducible]

instance DisjointUnion.instDecidableRelSumAdj {V₁ : Type u_1} {V₂ : Type u_2} (G : SimpleGraph V₁) (H : SimpleGraph V₂) [DecidableRel G.Adj] [DecidableRel H.Adj] : DecidableRel (G ⊕g H).Adj

theorem DisjointUnion.neighborFinset_sum_inl {V₁ : Type u_1} {V₂ : Type u_2} [Fintype V₁] [Fintype V₂] (G : SimpleGraph V₁) (H : SimpleGraph V₂) [DecidableRel G.Adj] [DecidableRel H.Adj] (v : V₁) : (G ⊕g H).neighborFinset (Sum.inl v) = Finset.map { toFun := Sum.inl, inj' := ⋯ } (G.neighborFinset v)

theorem DisjointUnion.neighborFinset_sum_inr {V₁ : Type u_1} {V₂ : Type u_2} [Fintype V₁] [Fintype V₂] (G : SimpleGraph V₁) (H : SimpleGraph V₂) [DecidableRel G.Adj] [DecidableRel H.Adj] (w : V₂) : (G ⊕g H).neighborFinset (Sum.inr w) = Finset.map { toFun := Sum.inr, inj' := ⋯ } (H.neighborFinset w)

theorem DisjointUnion.degree_sum_inl {V₁ : Type u_1} {V₂ : Type u_2} [Fintype V₁] [Fintype V₂] (G : SimpleGraph V₁) (H : SimpleGraph V₂) [DecidableRel G.Adj] [DecidableRel H.Adj] (v : V₁) : (G ⊕g H).degree (Sum.inl v) = G.degree v

theorem DisjointUnion.degree_sum_inr {V₁ : Type u_1} {V₂ : Type u_2} [Fintype V₁] [Fintype V₂] (G : SimpleGraph V₁) (H : SimpleGraph V₂) [DecidableRel G.Adj] [DecidableRel H.Adj] (w : V₂) : (G ⊕g H).degree (Sum.inr w) = H.degree w

theorem DisjointUnion.lapMatrix_sum_eq_fromBlocks {V₁ : Type u_1} {V₂ : Type u_2} [Fintype V₁] [Fintype V₂] [DecidableEq V₁] [DecidableEq V₂] (G : SimpleGraph V₁) (H : SimpleGraph V₂) [DecidableRel G.Adj] [DecidableRel H.Adj] : SimpleGraph.lapMatrix ℝ (G ⊕g H) = Matrix.fromBlocks (SimpleGraph.lapMatrix ℝ G) 0 0 (SimpleGraph.lapMatrix ℝ H)

theorem DisjointUnion.charpoly_roots_fromBlocks_zero {R : Type u_3} [CommRing R] [IsDomain R] {m : Type u_4} {n : Type u_5} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (A : Matrix m m R) (B : Matrix n n R) : (Matrix.fromBlocks A 0 0 B).charpoly.roots = A.charpoly.roots + B.charpoly.roots

theorem DisjointUnion.lapMatrix_sum_charpoly_roots {V₁ : Type u_1} {V₂ : Type u_2} [Fintype V₁] [Fintype V₂] [DecidableEq V₁] [DecidableEq V₂] (G : SimpleGraph V₁) (H : SimpleGraph V₂) [DecidableRel G.Adj] [DecidableRel H.Adj] : (SimpleGraph.lapMatrix ℝ (G ⊕g H)).charpoly.roots = (SimpleGraph.lapMatrix ℝ G).charpoly.roots + (SimpleGraph.lapMatrix ℝ H).charpoly.roots