IncMatrix

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

Statistics

Metric	Count
Definitions incMatrix	1
Theorems incMatrix_apply, incMatrix_apply', incMatrix_apply_eq_one_iff, incMatrix_apply_eq_zero_iff, incMatrix_apply_mul_incMatrix_apply, incMatrix_apply_mul_incMatrix_apply_of_not_adj, incMatrix_mul_transpose, incMatrix_mul_transpose_apply_of_adj, incMatrix_mul_transpose_diag, incMatrix_of_mem_incidenceSet, incMatrix_of_notMem_incidenceSet, incMatrix_transpose_mul_diag, sum_incMatrix_apply, sum_incMatrix_apply_of_mem_edgeSet, sum_incMatrix_apply_of_notMem_edgeSet	15
Total	16

SimpleGraph

Definitions

Name	Category	Theorems
incMatrix 📖	CompOp	15 math math: sum_incMatrix_apply, incMatrix_apply_mul_incMatrix_apply, incMatrix_apply_mul_incMatrix_apply_of_not_adj, incMatrix_apply', sum_incMatrix_apply_of_mem_edgeSet, incMatrix_mul_transpose, incMatrix_apply_eq_one_iff, incMatrix_mul_transpose_diag, incMatrix_transpose_mul_diag, incMatrix_of_notMem_incidenceSet, incMatrix_of_mem_incidenceSet, sum_incMatrix_apply_of_notMem_edgeSet, incMatrix_apply, incMatrix_apply_eq_zero_iff, incMatrix_mul_transpose_apply_of_adj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
incMatrix_apply 📖	mathematical	—	incMatrix Set.indicator Sym2 incidenceSet Pi.instOne	—	—
incMatrix_apply' 📖	mathematical	—	incMatrix Sym2 Set Set.instMembership incidenceSet decidableMemIncidenceSet	—	—
incMatrix_apply_eq_one_iff 📖	mathematical	—	incMatrix MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass Sym2 Set Set.instMembership incidenceSet	—	Ne.ite_eq_left_iff one_ne_zero NeZero.one
incMatrix_apply_eq_zero_iff 📖	mathematical	—	incMatrix MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass Sym2 Set Set.instMembership incidenceSet	—	incMatrix_apply NeZero.one
incMatrix_apply_mul_incMatrix_apply 📖	mathematical	—	MulZeroClass.toMul MulZeroOneClass.toMulZeroClass incMatrix MulZeroClass.toZero MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass Set.indicator Sym2 Set Set.instInter incidenceSet Pi.instOne	—	mul_ite mul_one MulZeroClass.mul_zero Set.indicator_apply
incMatrix_apply_mul_incMatrix_apply_of_not_adj 📖	mathematical	Adj	MulZeroClass.toMul MulZeroOneClass.toMulZeroClass incMatrix MulZeroClass.toZero MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	incMatrix_apply_mul_incMatrix_apply Set.indicator_of_notMem incidenceSet_inter_incidenceSet_of_not_adj Set.notMem_empty
incMatrix_mul_transpose 📖	mathematical	—	Matrix Sym2 Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid incMatrix MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Matrix.transpose DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Matrix.of AddMonoidWithOne.toNatCast degree Adj	—	Matrix.ext incMatrix_mul_transpose_diag incMatrix_mul_transpose_apply_of_adj Finset.sum_congr incMatrix_apply_mul_incMatrix_apply_of_not_adj Finset.sum_const_zero
incMatrix_mul_transpose_apply_of_adj 📖	mathematical	Adj	Matrix Sym2 Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid incMatrix MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Matrix.transpose	—	Finset.sum_congr incMatrix_apply_mul_incMatrix_apply Set.indicator_apply Finset.sum_boole Finset.coe_eq_singleton Finset.coe_filter_univ incidenceSet_inter_incidenceSet_of_adj Finset.card_singleton Nat.cast_one
incMatrix_mul_transpose_diag 📖	mathematical	—	Matrix Sym2 Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid incMatrix MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Matrix.transpose AddMonoidWithOne.toNatCast degree	—	sum_incMatrix_apply Finset.sum_congr mul_ite mul_one MulZeroClass.mul_zero Finset.sum_boole
incMatrix_of_mem_incidenceSet 📖	mathematical	Sym2 Set Set.instMembership incidenceSet	incMatrix MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	incMatrix_apply Set.indicator_of_mem Pi.one_apply
incMatrix_of_notMem_incidenceSet 📖	mathematical	Sym2 Set Set.instMembership incidenceSet	incMatrix MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	incMatrix_apply Set.indicator_of_notMem
incMatrix_transpose_mul_diag 📖	mathematical	—	Matrix Sym2 Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.transpose incMatrix MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Set Set.instMembership edgeSet instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Finset.sum_congr ite_zero_mul_ite_zero one_mul Finset.sum_boole Sym2.ind Nat.cast_two Finset.card_pair ne_of_adj Finset.filter.congr_simp mem_edgeSet Finset.ext Iff.not Finset.filter_false Nat.cast_zero
sum_incMatrix_apply 📖	mathematical	—	Finset.sum Sym2 NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Finset.univ incMatrix MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddMonoidWithOne.toNatCast degree	—	Finset.sum_congr Finset.sum_boole Set.filter_mem_univ_eq_toFinset Set.toFinset_card card_incidenceSet_eq_degree
sum_incMatrix_apply_of_mem_edgeSet 📖	mathematical	Sym2 Set Set.instMembership edgeSet	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Finset.univ incMatrix MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat	—	Sym2.ind Nat.instAtLeastTwoHAddOfNat Nat.cast_two Finset.card_pair Adj.ne mem_edgeSet Finset.sum_congr Finset.sum_boole Finset.ext Finset.filter.congr_simp
sum_incMatrix_apply_of_notMem_edgeSet 📖	mathematical	Sym2 Set Set.instMembership edgeSet	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Finset.univ incMatrix MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Finset.sum_eq_zero incMatrix_of_notMem_incidenceSet

---

← Back to Index