Theorems · Theorem · combinatorics

SimpleGraph.IsCompl.adjMatrix_add_adjMatrix_eq_adjMatrix_completeGraph

∀ (α : Type u_1) {V : Type u_2} {G : SimpleGraph V} [inst : DecidableRel G.Adj] [inst_1 : DecidableEq V]
  [inst_2 : AddZeroClass α] [inst_3 : One α] {H : SimpleGraph V} [inst_4 : DecidableRel H.Adj],
  IsCompl G H →
    SimpleGraph.adjMatrix α G + SimpleGraph.adjMatrix α H = SimpleGraph.adjMatrix α (SimpleGraph.completeGraph V)

Defined in: Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Cited by: 1 results in Mathlib
Foundations: Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: DecidableRel DecidableEq AddZeroClass One DecidableRel

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites12

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Matrixstatement and proof · cited by 4,303
SimpleGraphstatement and proof · cited by 3,072
Compl.complproof · cited by 2,925
add_zeroproof · cited by 2,707
zero_addproof · cited by 2,366
SimpleGraph.Adjstatement and proof · cited by 1,346
AddZeroClassstatement and proof · cited by 1,237
Matrix.extproof · cited by 540
IsComplstatement and proof · cited by 351
SimpleGraph.completeGraphstatement · cited by 49
SimpleGraph.adjMatrixstatement and proof · cited by 48
IsCompl.compl_eqproof · cited by 16

Cited by1

Results whose statement or proof uses this declaration.

SimpleGraph.adjMatrix_add_compl_adjMatrix_eq_adjMatrix_completeGraphproof · cited by 1