Documentation Verification Report

AdjMatrix

📁 Source: Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

Statistics

Metric	Count
Definitions `IsAdjMatrix`, `instDecidableRelAdjToGraphOfDecidableEq`, `toGraph`, `compl`, `adjMatrix`	5
Theorems `adjMatrix_toGraph_eq`, `apply_diag`, `apply_diag_ne`, `apply_ne_one_iff`, `apply_ne_zero_iff`, `compl`, `toGraph_adj`, `toGraph_compl_eq`, `zero_or_one`, `compl_apply`, `compl_apply_diag`, `isAdjMatrix_compl`, `isAdjMatrix_iff_hadamard`, `isSymm_compl`, `adjMatrix_apply`, `adjMatrix_dotProduct`, `adjMatrix_mulVec_apply`, `adjMatrix_mulVec_const_apply`, `adjMatrix_mulVec_const_apply_of_regular`, `adjMatrix_mul_apply`, `adjMatrix_mul_self_apply_self`, `adjMatrix_pow_apply_eq_card_walk`, `adjMatrix_vecMul_apply`, `dotProduct_adjMatrix`, `dotProduct_mulVec_adjMatrix`, `isAdjMatrix_adjMatrix`, `isSymm_adjMatrix`, `mul_adjMatrix_apply`, `one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes`, `toGraph_adjMatrix_eq`, `trace_adjMatrix`, `transpose_adjMatrix`	32
Total	37

Matrix

Definitions

Name	Category	Theorems
`IsAdjMatrix` 📖	CompData	3 math math: `SimpleGraph.isAdjMatrix_adjMatrix`, `isAdjMatrix_iff_hadamard`, `isAdjMatrix_compl`
`compl` 📖	CompOp	7 math math: `IsAdjMatrix.compl`, `compl_apply`, `compl_apply_diag`, `IsAdjMatrix.toGraph_compl_eq`, `isSymm_compl`, `SimpleGraph.one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes`, `isAdjMatrix_compl`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compl_apply` 📖	mathematical	—	`compl`	—	—
`compl_apply_diag` 📖	mathematical	—	`compl`	—	—
`isAdjMatrix_compl` 📖	mathematical	`IsSymm`	`IsAdjMatrix` `compl`	—	`compl_apply_diag`
`isAdjMatrix_iff_hadamard` 📖	mathematical	—	`IsAdjMatrix` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `hadamard` `MulZeroClass.toMul` `IsSymm` `Matrix` `one` `zero`	—	—
`isSymm_compl` 📖	mathematical	`IsSymm`	`compl`	—	`ext` `IsSymm.apply`

Matrix.IsAdjMatrix

Definitions

Name	Category	Theorems
`instDecidableRelAdjToGraphOfDecidableEq` 📖	CompOp	1 math math: `adjMatrix_toGraph_eq`
`toGraph` 📖	CompOp	4 math math: `toGraph_adj`, `SimpleGraph.toGraph_adjMatrix_eq`, `toGraph_compl_eq`, `adjMatrix_toGraph_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjMatrix_toGraph_eq` 📖	mathematical	`Matrix.IsAdjMatrix` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	`SimpleGraph.adjMatrix` `toGraph` `instDecidableRelAdjToGraphOfDecidableEq`	—	`Matrix.ext` `zero_or_one` `NeZero.one`
`apply_diag` 📖	—	`Matrix.IsAdjMatrix`	—	—	—
`apply_diag_ne` 📖	—	`Matrix.IsAdjMatrix` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	—	—	`apply_diag` `NeZero.one`
`apply_ne_one_iff` 📖	—	`Matrix.IsAdjMatrix` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	—	—	`zero_or_one` `NeZero.one`
`apply_ne_zero_iff` 📖	—	`Matrix.IsAdjMatrix` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	—	—	`apply_ne_one_iff`
`compl` 📖	mathematical	`Matrix.IsAdjMatrix`	`Matrix.compl`	—	`Matrix.isAdjMatrix_compl` `symm`
`toGraph_adj` 📖	mathematical	`Matrix.IsAdjMatrix` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	`SimpleGraph.Adj` `toGraph`	—	—
`toGraph_compl_eq` 📖	mathematical	`Matrix.IsAdjMatrix` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	`toGraph` `Matrix.compl` `compl` `Compl.compl` `SimpleGraph` `SimpleGraph.instCompl`	—	`SimpleGraph.ext` `compl` `zero_or_one` `NeZero.one`
`zero_or_one` 📖	—	`Matrix.IsAdjMatrix`	—	—	—

SimpleGraph

Definitions

Name	Category	Theorems
`adjMatrix` 📖	CompOp	20 math math: `adjMatrix_mulVec_apply`, `adjMatrix_apply`, `isAdjMatrix_adjMatrix`, `dotProduct_mulVec_adjMatrix`, `mul_adjMatrix_apply`, `isSymm_adjMatrix`, `IsSRGWith.matrix_eq`, `adjMatrix_pow_apply_eq_card_walk`, `dotProduct_adjMatrix`, `toGraph_adjMatrix_eq`, `adjMatrix_mulVec_const_apply`, `adjMatrix_mul_apply`, `adjMatrix_mulVec_const_apply_of_regular`, `adjMatrix_vecMul_apply`, `adjMatrix_mul_self_apply_self`, `one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes`, `adjMatrix_dotProduct`, `transpose_adjMatrix`, `Matrix.IsAdjMatrix.adjMatrix_toGraph_eq`, `trace_adjMatrix`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjMatrix_apply` 📖	mathematical	—	`adjMatrix` `Adj`	—	—
`adjMatrix_dotProduct` 📖	mathematical	—	`dotProduct` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `adjMatrix` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Finset.sum` `neighborFinset` `neighborSetFintype`	—	`Finset.sum_congr` `ite_mul` `one_mul` `MulZeroClass.zero_mul` `neighborFinset_eq_filter` `Finset.sum_filter`
`adjMatrix_mulVec_apply` 📖	mathematical	—	`Matrix.mulVec` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `adjMatrix` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `neighborFinset` `neighborSetFintype`	—	`Matrix.mulVec.eq_1` `adjMatrix_dotProduct`
`adjMatrix_mulVec_const_apply` 📖	mathematical	—	`Matrix.mulVec` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `adjMatrix` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toNatCast` `degree` `neighborSetFintype`	—	`adjMatrix_mulVec_apply` `Finset.sum_congr` `Finset.sum_const` `nsmul_eq_mul`
`adjMatrix_mulVec_const_apply_of_regular` 📖	mathematical	`IsRegularOfDegree` `neighborSetFintype`	`Matrix.mulVec` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `adjMatrix` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toNatCast`	—	`adjMatrix_mulVec_apply` `Finset.sum_congr` `Finset.sum_const` `nsmul_eq_mul`
`adjMatrix_mul_apply` 📖	mathematical	—	`Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `adjMatrix` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Finset.sum` `neighborFinset` `neighborSetFintype`	—	`Finset.sum_congr` `ite_mul` `one_mul` `MulZeroClass.zero_mul` `neighborFinset_eq_filter` `Finset.sum_filter`
`adjMatrix_mul_self_apply_self` 📖	mathematical	—	`Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `adjMatrix` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddMonoidWithOne.toNatCast` `degree` `neighborSetFintype`	—	`mul_adjMatrix_apply` `Finset.sum_congr` `Finset.sum_boole` `Finset.filter_true_of_mem`
`adjMatrix_pow_apply_eq_card_walk` 📖	mathematical	—	`Matrix` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `adjMatrix` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddMonoidWithOne.toNatCast` `Fintype.card` `Set.Elem` `Walk` `setOf` `Walk.length` `fintypeSetWalkLength` `neighborSetFintype`	—	`card_set_walk_length_eq` `eq_or_ne` `pow_zero` `Matrix.one_apply_eq` `Finset.card_singleton` `Nat.cast_one` `Matrix.one_apply_ne` `Nat.cast_zero` `pow_succ'` `adjMatrix_mul_apply` `Finset.sum_congr` `Finset.card_biUnion` `Function.onFun.eq_1` `disjoint_iff_inf_le` `Nat.cast_sum` `Finset.card_map` `Finset.sum_toFinset_eq_subtype`
`adjMatrix_vecMul_apply` 📖	mathematical	—	`Matrix.vecMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `adjMatrix` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `neighborFinset` `neighborSetFintype`	—	`Matrix.transpose_apply` `transpose_adjMatrix`
`dotProduct_adjMatrix` 📖	mathematical	—	`dotProduct` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `adjMatrix` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Finset.sum` `neighborFinset` `neighborSetFintype`	—	`Finset.sum_congr` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `neighborFinset_eq_filter` `Finset.sum_filter`
`dotProduct_mulVec_adjMatrix` 📖	mathematical	—	`dotProduct` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.mulVec` `adjMatrix` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Finset.sum` `Finset.univ` `Adj`	—	`Finset.sum_congr` `ite_mul` `one_mul` `MulZeroClass.zero_mul` `Finset.mul_sum` `mul_ite` `MulZeroClass.mul_zero`
`isAdjMatrix_adjMatrix` 📖	mathematical	—	`Matrix.IsAdjMatrix` `adjMatrix`	—	—
`isSymm_adjMatrix` 📖	mathematical	—	`Matrix.IsSymm` `adjMatrix`	—	`transpose_adjMatrix`
`mul_adjMatrix_apply` 📖	mathematical	—	`Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `adjMatrix` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Finset.sum` `neighborFinset` `neighborSetFintype`	—	`Finset.sum_congr` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `neighborFinset_eq_filter` `Finset.sum_filter`
`one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes` 📖	mathematical	—	`Matrix` `Matrix.add` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddMonoidWithOne.toAddMonoid` `Matrix.one` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toOne` `adjMatrix` `Matrix.compl` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Matrix.of`	—	`Matrix.ext` `Matrix.of_apply` `Matrix.add_apply` `adjMatrix_apply` `Matrix.one_apply` `add_zero` `zero_add`
`toGraph_adjMatrix_eq` 📖	mathematical	—	`Matrix.IsAdjMatrix.toGraph` `adjMatrix` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `isAdjMatrix_adjMatrix`	—	`ext` `isAdjMatrix_adjMatrix` `NeZero.one`
`trace_adjMatrix` 📖	mathematical	—	`Matrix.trace` `adjMatrix` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`Finset.sum_congr` `Finset.sum_const_zero`
`transpose_adjMatrix` 📖	mathematical	—	`Matrix.transpose` `adjMatrix`	—	`Matrix.ext`

---

← Back to Index