Mathlib Map

Theorems · Theorem · combinatorics

Matrix.IsAdjMatrix.isHermitian

∀ {α : Type u_1} {V : Type u_2} [inst : NonAssocSemiring α] [inst_1 : StarRing α] {A : Matrix V V α},
  A.IsAdjMatrix → A.IsHermitian
Defined in
Mathlib.Combinatorics.SimpleGraph.LapMatrix
Cited by
1 results in Mathlib
Foundations
Depth 20 from the axioms · uses propext, Quot.sound
Assumes
NonAssocSemiringStarRing
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

SimpleGraph.isHermitian_adjMatrix · cited by 1SimpleGraph.isHermitian_a…Matrix · cited by 4303MatrixStarRing · cited by 1686StarRingStar.star · cited by 1082Star.starNonAssocSemiring · cited by 805NonAssocSemiringMatrix.ext · cited by 540Matrix.extMatrix.IsHermitian · cited by 126Matrix.IsHermitianstar_zero · cited by 58star_zerostar_one · cited by 33star_oneMatrix.IsAdjMatrix · cited by 28Matrix.IsAdjMatrixMatrix.IsAdjMatrix.zero_or_one · cited by 6IsAdjMatrix.zero_or_oneMatrix.IsSymm.apply · cited by 4IsSymm.applyMatrix.IsAdjMatrix.symm · cited by 3IsAdjMatrix.symmIsAdjMatrix.isHermitianCITED BYCITES

Cites12

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

Cited by1

Results whose statement or proof uses this declaration.