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`, `compl_compl`, `compl_inj`, `hadamard_self`, `toGraph_adj`, `toGraph_compl_eq`, `zero`, `zero_or_one`, `compl_apply`, `compl_apply_diag`, `compl_of_one_sub_one`, `compl_zero`, `compl_zero_eq_of_one_sub_one`, `isAdjMatrix_compl`, `isAdjMatrix_iff_hadamard`, `isSymm_compl`, `adjMatrix_add_adjMatrix_eq_adjMatrix_completeGraph`, `adjMatrix_add_compl_adjMatrix_eq_adjMatrix_completeGraph`, `adjMatrix_apply`, `adjMatrix_bot`, `adjMatrix_completeGraph_eq_of_one_sub_one`, `adjMatrix_dotProduct`, `adjMatrix_hadamard_diagonal`, `adjMatrix_hadamard_intCast`, `adjMatrix_hadamard_natCast`, `adjMatrix_hadamard_ofNat`, `adjMatrix_hadamard_one`, `adjMatrix_hadamard_self`, `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_top`, `adjMatrix_vecMul_apply`, `compl_adjMatrix_completeGraph`, `compl_adjMatrix_eq_adjMatrix_compl`, `diag_adjMatrix`, `diagonal_hadamard_adjMatrix`, `dotProduct_adjMatrix`, `dotProduct_mulVec_adjMatrix`, `intCast_hadamard_adjMatrix`, `isAdjMatrix_adjMatrix`, `isSymm_adjMatrix`, `mul_adjMatrix_apply`, `natCast_card_dart_eq_dotProduct`, `natCast_hadamard_adjMatrix`, `ofNat_hadamard_adjMatrix`, `one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes`, `one_add_adjMatrix_add_compl_adjMatrix_eq_of_one`, `one_hadamard_adjMatrix`, `toGraph_adjMatrix_eq`, `trace_adjMatrix`, `transpose_adjMatrix`	60
Total	65

Matrix

Definitions

Name	Category	Theorems
`IsAdjMatrix` 📖	CompData	5 math math: `SimpleGraph.isAdjMatrix_adjMatrix`, `IsAdjMatrix.compl`, `IsAdjMatrix.zero`, `isAdjMatrix_iff_hadamard`, `isAdjMatrix_compl`
`compl` 📖	CompOp	16 math math: `SimpleGraph.one_add_adjMatrix_add_compl_adjMatrix_eq_of_one`, `IsAdjMatrix.compl`, `compl_apply`, `SimpleGraph.compl_adjMatrix_completeGraph`, `IsAdjMatrix.compl_inj`, `compl_apply_diag`, `IsAdjMatrix.compl_compl`, `IsAdjMatrix.toGraph_compl_eq`, `compl_of_one_sub_one`, `isSymm_compl`, `compl_zero`, `SimpleGraph.one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes`, `isAdjMatrix_compl`, `SimpleGraph.compl_adjMatrix_eq_adjMatrix_compl`, `SimpleGraph.adjMatrix_add_compl_adjMatrix_eq_adjMatrix_completeGraph`, `compl_zero_eq_of_one_sub_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compl_apply` 📖	mathematical	—	`compl`	—	—
`compl_apply_diag` 📖	mathematical	—	`compl`	—	—
`compl_of_one_sub_one` 📖	mathematical	—	`compl` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Matrix` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `Pi.instOne` `one` `zero`	—	`SimpleGraph.compl_adjMatrix_completeGraph`
`compl_zero` 📖	mathematical	—	`compl` `Matrix` `zero` `SimpleGraph.adjMatrix` `SimpleGraph.completeGraph` `SimpleGraph.Top.adjDecidable`	—	`IsAdjMatrix.compl_compl` `SimpleGraph.compl_adjMatrix_completeGraph`
`compl_zero_eq_of_one_sub_one` 📖	mathematical	—	`compl` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Matrix` `zero` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `Pi.instOne` `one`	—	`compl_zero` `SimpleGraph.adjMatrix_completeGraph_eq_of_one_sub_one`
`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`	`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` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	—	`Matrix.ext` `zero_or_one` `NeZero.one`
`apply_diag` 📖	—	`Matrix.IsAdjMatrix`	—	—	—
`apply_diag_ne` 📖	mathematical	`Matrix.IsAdjMatrix` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	`MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	—	`apply_diag` `NeZero.one`
`apply_ne_one_iff` 📖	mathematical	`Matrix.IsAdjMatrix` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	`MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass`	—	`zero_or_one` `NeZero.one`
`apply_ne_zero_iff` 📖	mathematical	`Matrix.IsAdjMatrix` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	`MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	—	`apply_ne_one_iff`
`compl` 📖	mathematical	`Matrix.IsAdjMatrix`	`Matrix.IsAdjMatrix` `Matrix.compl`	—	`Matrix.isAdjMatrix_compl` `symm`
`compl_compl` 📖	mathematical	`Matrix.IsAdjMatrix`	`Matrix.compl`	—	`Matrix.ext`
`compl_inj` 📖	mathematical	`Matrix.IsAdjMatrix`	`Matrix.compl`	—	`Matrix.ext`
`hadamard_self` 📖	mathematical	`Matrix.IsAdjMatrix` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	`Matrix.hadamard` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass`	—	`Matrix.ext` `zero_or_one` `MulZeroClass.mul_zero` `mul_one`
`toGraph_adj` 📖	mathematical	`Matrix.IsAdjMatrix` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	`SimpleGraph.Adj` `toGraph` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	—	—
`toGraph_compl_eq` 📖	mathematical	`Matrix.IsAdjMatrix` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	`toGraph` `Matrix.compl` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `compl` `Compl.compl` `SimpleGraph` `SimpleGraph.instCompl`	—	`SimpleGraph.ext` `compl` `zero_or_one` `NeZero.one`
`zero` 📖	mathematical	—	`Matrix.IsAdjMatrix` `Matrix` `Matrix.zero`	—	—
`zero_or_one` 📖	—	`Matrix.IsAdjMatrix`	—	—	—

SimpleGraph

Definitions

Name	Category	Theorems
`adjMatrix` 📖	CompOp	43 math math: `adjMatrix_mulVec_apply`, `adjMatrix_apply`, `isAdjMatrix_adjMatrix`, `one_add_adjMatrix_add_compl_adjMatrix_eq_of_one`, `dotProduct_mulVec_adjMatrix`, `adjMatrix_hadamard_ofNat`, `isHermitian_adjMatrix`, `mul_adjMatrix_apply`, `natCast_card_dart_eq_dotProduct`, `adjMatrix_hadamard_intCast`, `adjMatrix_hadamard_diagonal`, `intCast_hadamard_adjMatrix`, `isSymm_adjMatrix`, `compl_adjMatrix_completeGraph`, `diagonal_hadamard_adjMatrix`, `IsSRGWith.matrix_eq`, `one_hadamard_adjMatrix`, `adjMatrix_pow_apply_eq_card_walk`, `dotProduct_adjMatrix`, `toGraph_adjMatrix_eq`, `ofNat_hadamard_adjMatrix`, `adjMatrix_mulVec_const_apply`, `adjMatrix_mul_apply`, `adjMatrix_hadamard_self`, `IsCompl.adjMatrix_add_adjMatrix_eq_adjMatrix_completeGraph`, `adjMatrix_mulVec_const_apply_of_regular`, `adjMatrix_vecMul_apply`, `adjMatrix_bot`, `adjMatrix_completeGraph_eq_of_one_sub_one`, `adjMatrix_mul_self_apply_self`, `Matrix.compl_zero`, `one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes`, `adjMatrix_dotProduct`, `adjMatrix_top`, `transpose_adjMatrix`, `adjMatrix_hadamard_natCast`, `Matrix.IsAdjMatrix.adjMatrix_toGraph_eq`, `compl_adjMatrix_eq_adjMatrix_compl`, `diag_adjMatrix`, `natCast_hadamard_adjMatrix`, `trace_adjMatrix`, `adjMatrix_hadamard_one`, `adjMatrix_add_compl_adjMatrix_eq_adjMatrix_completeGraph`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjMatrix_add_compl_adjMatrix_eq_adjMatrix_completeGraph` 📖	mathematical	—	`Matrix` `Matrix.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `adjMatrix` `AddZero.toZero` `Matrix.compl` `completeGraph` `Top.adjDecidable`	—	`IsCompl.adjMatrix_add_adjMatrix_eq_adjMatrix_completeGraph` `isCompl_compl` `compl_adjMatrix_eq_adjMatrix_compl`
`adjMatrix_apply` 📖	mathematical	—	`adjMatrix` `Adj`	—	—
`adjMatrix_bot` 📖	mathematical	—	`adjMatrix` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `Bot.adjDecidable` `Matrix` `Matrix.zero`	—	`Matrix.ext`
`adjMatrix_completeGraph_eq_of_one_sub_one` 📖	mathematical	—	`adjMatrix` `completeGraph` `Top.adjDecidable` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Matrix` `Matrix.sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Matrix.of` `Pi.instOne` `Matrix.one`	—	`Matrix.ext` `sub_ite` `sub_self` `sub_zero`
`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_hadamard_diagonal` 📖	mathematical	—	`Matrix.hadamard` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `adjMatrix` `MulZeroClass.toZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `Matrix.diagonal` `Matrix` `Matrix.zero`	—	`Matrix.hadamard_diagonal` `diag_adjMatrix` `MulZeroClass.zero_mul` `Matrix.diagonal_zero'`
`adjMatrix_hadamard_intCast` 📖	mathematical	—	`Matrix.hadamard` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `adjMatrix` `MulZeroClass.toZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `Matrix` `Matrix.instIntCastOfZero` `Matrix.zero`	—	`adjMatrix_hadamard_diagonal`
`adjMatrix_hadamard_natCast` 📖	mathematical	—	`Matrix.hadamard` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `adjMatrix` `MulZeroClass.toZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `Matrix` `Matrix.instNatCastOfZero` `Matrix.zero`	—	`adjMatrix_hadamard_diagonal`
`adjMatrix_hadamard_ofNat` 📖	mathematical	—	`Matrix.hadamard` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `adjMatrix` `MulZeroClass.toZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `Matrix` `Matrix.zero`	—	`adjMatrix_hadamard_diagonal`
`adjMatrix_hadamard_one` 📖	mathematical	—	`Matrix.hadamard` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `adjMatrix` `MulZeroClass.toZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `Matrix` `Matrix.one` `Matrix.zero`	—	`adjMatrix_hadamard_diagonal`
`adjMatrix_hadamard_self` 📖	mathematical	—	`Matrix.hadamard` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `adjMatrix` `MulZeroClass.toZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	—	`Matrix.IsAdjMatrix.hadamard_self`
`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.toPow` `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_top` 📖	mathematical	—	`adjMatrix` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `Top.adjDecidable` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `Matrix.of`	—	`Matrix.ext` `eq_or_ne` `adjMatrix.congr_simp`
`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`
`compl_adjMatrix_completeGraph` 📖	mathematical	—	`Matrix.compl` `adjMatrix` `completeGraph` `Top.adjDecidable` `Matrix` `Matrix.zero`	—	—
`compl_adjMatrix_eq_adjMatrix_compl` 📖	mathematical	—	`Matrix.compl` `adjMatrix` `Compl.compl` `SimpleGraph` `instCompl` `Compl.adjDecidable`	—	`Matrix.ext`
`diag_adjMatrix` 📖	mathematical	—	`Matrix.diag` `adjMatrix` `Pi.instZero`	—	—
`diagonal_hadamard_adjMatrix` 📖	mathematical	—	`Matrix.hadamard` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `Matrix.diagonal` `MulZeroClass.toZero` `adjMatrix` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `Matrix` `Matrix.zero`	—	`Matrix.diagonal_hadamard` `diag_adjMatrix` `MulZeroClass.mul_zero` `Matrix.diagonal_zero'`
`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`
`intCast_hadamard_adjMatrix` 📖	mathematical	—	`Matrix.hadamard` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `Matrix` `Matrix.instIntCastOfZero` `MulZeroClass.toZero` `adjMatrix` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `Matrix.zero`	—	`diagonal_hadamard_adjMatrix`
`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`
`natCast_card_dart_eq_dotProduct` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Fintype.card` `Dart` `Dart.fintype` `dotProduct` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.mulVec` `adjMatrix` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `Pi.instOne`	—	`dart_card_eq_sum_degrees` `Nat.cast_sum` `dotProduct_one` `Finset.sum_congr` `adjMatrix_mulVec_apply` `Finset.sum_const` `nsmul_eq_mul` `mul_one`
`natCast_hadamard_adjMatrix` 📖	mathematical	—	`Matrix.hadamard` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `Matrix` `Matrix.instNatCastOfZero` `MulZeroClass.toZero` `adjMatrix` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `Matrix.zero`	—	`diagonal_hadamard_adjMatrix`
`ofNat_hadamard_adjMatrix` 📖	mathematical	—	`Matrix.hadamard` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `adjMatrix` `MulZeroClass.toZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `Matrix` `Matrix.zero`	—	`diagonal_hadamard_adjMatrix`
`one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes` 📖	mathematical	—	`Matrix` `Matrix.add` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `Matrix.one` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `adjMatrix` `Matrix.compl` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Matrix.of` `Pi.instOne`	—	`one_add_adjMatrix_add_compl_adjMatrix_eq_of_one`
`one_add_adjMatrix_add_compl_adjMatrix_eq_of_one` 📖	mathematical	—	`Matrix` `Matrix.add` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `Matrix.one` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `adjMatrix` `Matrix.compl` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Matrix.of` `Pi.instOne`	—	`add_assoc` `adjMatrix_add_compl_adjMatrix_eq_adjMatrix_completeGraph` `Matrix.ext` `Matrix.one_apply_ne` `zero_add` `Matrix.one_apply_eq` `add_zero`
`one_hadamard_adjMatrix` 📖	mathematical	—	`Matrix.hadamard` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `Matrix` `Matrix.one` `MulZeroClass.toZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `adjMatrix` `Matrix.zero`	—	`diagonal_hadamard_adjMatrix`
`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`

SimpleGraph.IsCompl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjMatrix_add_adjMatrix_eq_adjMatrix_completeGraph` 📖	mathematical	`IsCompl` `SimpleGraph` `SimpleGraph.instPartialOrder` `CompleteLattice.toBoundedOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `SimpleGraph.completeAtomicBooleanAlgebra`	`Matrix` `Matrix.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `SimpleGraph.adjMatrix` `AddZero.toZero` `SimpleGraph.completeGraph` `SimpleGraph.Top.adjDecidable`	—	`IsCompl.compl_eq` `Matrix.ext` `zero_add` `add_zero`

---

← Back to Index