Theorems · Theorem · combinatorics

Matrix.IsAdjMatrix.reindex

∀ {α : Type u_1} {V : Type u_2} {W : Type u_3} {A : Matrix V V α} [inst : Zero α] [inst_1 : One α],
  A.IsAdjMatrix → ∀ (f : V ≃ W), ((Matrix.reindex f f) A).IsAdjMatrix

Defined in

Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Cited by

2 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Quot.sound

Assumes

ZeroOne