IncidenceAlgebra

📁 Source: Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean

Statistics

Metric	Count
Definitions `IncidenceAlgebra`, `algebraRight`, `eulerChar`, `instAdd`, `instAddCommGroup`, `instAddCommMonoid`, `instAddGroup`, `instAddMonoid`, `instFunLike`, `instInhabited`, `instModule`, `instMul`, `instNeg`, `instNonAssocSemiring`, `instNonUnitalNonAssocSemiring`, `instOne`, `instRing`, `instSMul`, `instSemiring`, `instSmulZeroClassRight`, `instSub`, `instZero`, `lambda`, `moduleRight`, `mu`, `prod`, `smulWithZeroRight`, `toFun`, `zeta`	29
Theorems `add_apply`, `apply_eq_zero_of_not_le`, `coe_add`, `coe_constSMul`, `coe_inj`, `coe_mk`, `coe_neg`, `coe_sub`, `coe_zero`, `constSMul_apply`, `eq_zero_of_not_le'`, `eulerChar_orderDual`, `eulerChar_prod`, `ext`, `ext_iff`, `instIsScalarTower`, `lambda_apply`, `le_of_ne_zero`, `mk_coe`, `moebius_inversion_bot`, `moebius_inversion_top`, `mu_apply`, `mu_eq_neg_sum_Ico_of_ne`, `mu_eq_neg_sum_Ioc_of_ne`, `mu_mul_zeta`, `mu_ofDual`, `mu_prod_mu`, `mu_self`, `mu_toDual`, `mul_apply`, `neg_apply`, `one_apply`, `one_prod_one`, `prod_apply`, `prod_mk`, `prod_mul_prod`, `prod_mul_prod'`, `smul_apply`, `sub_apply`, `sum_Icc_mu_left`, `sum_Icc_mu_right`, `toFun_eq_coe`, `zero_apply`, `zeta_apply`, `zeta_mul_kappa`, `zeta_mul_mu`, `zeta_mul_zeta`, `zeta_of_le`, `zeta_prod_apply`, `zeta_prod_mk`, `zeta_prod_zeta`	51
Total	80

IncidenceAlgebra

Definitions

Name	Category	Theorems
`algebraRight` 📖	CompOp	—
`eulerChar` 📖	CompOp	2 math math: `eulerChar_prod`, `eulerChar_orderDual`
`instAdd` 📖	CompOp	2 math math: `add_apply`, `coe_add`
`instAddCommGroup` 📖	CompOp	—
`instAddCommMonoid` 📖	CompOp	—
`instAddGroup` 📖	CompOp	—
`instAddMonoid` 📖	CompOp	—
`instFunLike` 📖	CompOp	37 math math: `prod_mk`, `constSMul_apply`, `coe_constSMul`, `zeta_mul_kappa`, `moebius_inversion_top`, `coe_sub`, `one_apply`, `zeta_of_le`, `zeta_mul_zeta`, `neg_apply`, `mul_apply`, `coe_zero`, `moebius_inversion_bot`, `apply_eq_zero_of_not_le`, `add_apply`, `mu_apply`, `mu_ofDual`, `smul_apply`, `coe_inj`, `coe_add`, `prod_apply`, `coe_neg`, `sum_Icc_mu_left`, `zero_apply`, `zeta_prod_apply`, `sum_Icc_mu_right`, `mu_eq_neg_sum_Ioc_of_ne`, `zeta_apply`, `toFun_eq_coe`, `lambda_apply`, `sub_apply`, `mu_eq_neg_sum_Ico_of_ne`, `coe_mk`, `mu_toDual`, `ext_iff`, `mu_self`, `zeta_prod_mk`
`instInhabited` 📖	CompOp	—
`instModule` 📖	CompOp	—
`instMul` 📖	CompOp	7 math math: `zeta_mul_kappa`, `zeta_mul_zeta`, `mul_apply`, `mu_mul_zeta`, `zeta_mul_mu`, `prod_mul_prod'`, `prod_mul_prod`
`instNeg` 📖	CompOp	2 math math: `neg_apply`, `coe_neg`
`instNonAssocSemiring` 📖	CompOp	—
`instNonUnitalNonAssocSemiring` 📖	CompOp	—
`instOne` 📖	CompOp	4 math math: `one_apply`, `one_prod_one`, `mu_mul_zeta`, `zeta_mul_mu`
`instRing` 📖	CompOp	—
`instSMul` 📖	CompOp	2 math math: `instIsScalarTower`, `smul_apply`
`instSemiring` 📖	CompOp	—
`instSmulZeroClassRight` 📖	CompOp	2 math math: `constSMul_apply`, `coe_constSMul`
`instSub` 📖	CompOp	2 math math: `coe_sub`, `sub_apply`
`instZero` 📖	CompOp	4 math math: `constSMul_apply`, `coe_constSMul`, `coe_zero`, `zero_apply`
`lambda` 📖	CompOp	1 math math: `lambda_apply`
`moduleRight` 📖	CompOp	—
`mu` 📖	CompOp	13 math math: `moebius_inversion_top`, `moebius_inversion_bot`, `mu_apply`, `mu_ofDual`, `sum_Icc_mu_left`, `sum_Icc_mu_right`, `mu_eq_neg_sum_Ioc_of_ne`, `mu_mul_zeta`, `zeta_mul_mu`, `mu_eq_neg_sum_Ico_of_ne`, `mu_prod_mu`, `mu_toDual`, `mu_self`
`prod` 📖	CompOp	7 math math: `prod_mk`, `prod_apply`, `one_prod_one`, `prod_mul_prod'`, `mu_prod_mu`, `prod_mul_prod`, `zeta_prod_zeta`
`smulWithZeroRight` 📖	CompOp	—
`toFun` 📖	CompOp	2 math math: `eq_zero_of_not_le'`, `toFun_eq_coe`
`zeta` 📖	CompOp	9 math math: `zeta_mul_kappa`, `zeta_of_le`, `zeta_mul_zeta`, `zeta_prod_apply`, `mu_mul_zeta`, `zeta_mul_mu`, `zeta_apply`, `zeta_prod_mk`, `zeta_prod_zeta`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `instFunLike` `instAdd` `AddZero.toAdd`	—	—
`apply_eq_zero_of_not_le` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `instFunLike`	—	`eq_zero_of_not_le'`
`coe_add` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `instFunLike` `instAdd` `Pi.instAdd` `AddZero.toAdd`	—	—
`coe_constSMul` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `instFunLike` `SMulZeroClass.toSMul` `instZero` `instSmulZeroClassRight` `Function.hasSMul`	—	—
`coe_inj` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `instFunLike`	—	`DFunLike.coe_injective`
`coe_mk` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `instFunLike`	—	—
`coe_neg` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `instFunLike` `instNeg` `Pi.instNeg` `NegZeroClass.toNeg`	—	—
`coe_sub` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `instFunLike` `instSub` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	—
`coe_zero` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `instFunLike` `instZero` `Pi.instZero`	—	—
`constSMul_apply` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `instFunLike` `SMulZeroClass.toSMul` `instZero` `instSmulZeroClassRight`	—	—
`eq_zero_of_not_le'` 📖	mathematical	—	`toFun`	—	—
`eulerChar_orderDual` 📖	mathematical	—	`eulerChar` `OrderDual` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `OrderDual.instPreorder` `PartialOrder.toPreorder` `OrderDual.instLocallyFiniteOrder` `OrderDual.instBoundedOrder` `Preorder.toLE`	—	`mu_toDual`
`eulerChar_prod` 📖	mathematical	—	`eulerChar` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Prod.instPreorder` `PartialOrder.toPreorder` `Prod.instLocallyFiniteOrder` `Prod.instDecidableLE` `Preorder.toLE` `Prod.instBoundedOrder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—
`ext` 📖	—	`DFunLike.coe` `IncidenceAlgebra` `instFunLike`	—	—	`DFunLike.coe_injective'` `apply_eq_zero_of_not_le`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `instFunLike`	—	`ext`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `IncidenceAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Preorder.toLE` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSMul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`ext` `Finset.sum_congr` `Finset.sum_smul` `Finset.sum_sigma'` `Finset.smul_sum` `Finset.sum_nbij'` `le_trans` `Sigma.eta` `smul_assoc`
`lambda_apply` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `Preorder.toLE` `instFunLike` `lambda` `WCovBy`	—	—
`le_of_ne_zero` 📖	—	—	—	—	`not_imp_comm` `apply_eq_zero_of_not_le`
`mk_coe` 📖	—	`DFunLike.coe` `IncidenceAlgebra` `instFunLike`	—	—	—
`moebius_inversion_bot` 📖	mathematical	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finset.Iic` `PartialOrder.toPreorder` `LocallyFiniteOrder.toLocallyFiniteOrderBot`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `IncidenceAlgebra` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Preorder.toLE` `instFunLike` `mu` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`Finset.sum_congr` `mu_toDual` `moebius_inversion_top`
`moebius_inversion_top` 📖	mathematical	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finset.Ici` `PartialOrder.toPreorder` `LocallyFiniteOrder.toLocallyFiniteOrderTop`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `IncidenceAlgebra` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Preorder.toLE` `instFunLike` `mu` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`Finset.sum_congr` `zeta_apply` `Finset.mem_Ici` `one_mul` `ite_mul` `MulZeroClass.zero_mul` `Finset.mul_sum` `mul_ite` `MulZeroClass.mul_zero` `mul_one` `Finset.sum_sigma'` `mul_boole` `Finset.sum_nbij'` `le_trans` `Sigma.eta` `Finset.sum_mul` `mu_mul_zeta` `Finset.sum_ite_eq` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Finset.sum_eq_zero` `LT.lt.not_ge` `Finset.mem_Ioi`
`mu_apply` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Preorder.toLE` `instFunLike` `mu` `NegZeroClass.toNeg` `Finset.sum` `AddCommGroup.toAddCommMonoid` `Finset.Ico`	—	`mu.eq_1` `Finset.sum_attach`
`mu_eq_neg_sum_Ico_of_ne` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Preorder.toLE` `instFunLike` `mu` `NegZeroClass.toNeg` `Finset.sum` `AddCommGroup.toAddCommMonoid` `Finset.Ico`	—	`mu_apply`
`mu_eq_neg_sum_Ioc_of_ne` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Preorder.toLE` `PartialOrder.toPreorder` `instFunLike` `mu` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NegZeroClass.toNeg` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finset.Ioc`	—	—
`mu_mul_zeta` 📖	mathematical	—	`IncidenceAlgebra` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instMul` `AddCommGroup.toAddCommMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `mu` `MulOne.toOne` `zeta` `instOne`	—	`ext` `mul_apply` `Finset.sum_congr` `Finset.mem_Icc` `mul_one` `sum_Icc_mu_right`
`mu_ofDual` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Preorder.toLE` `PartialOrder.toPreorder` `instFunLike` `mu` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Equiv` `OrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `OrderDual.instPreorder` `OrderDual.instLocallyFiniteOrder`	—	`mu_toDual`
`mu_prod_mu` 📖	mathematical	—	`prod` `PartialOrder.toPreorder` `mu` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Prod.instPreorder` `Prod.instLocallyFiniteOrder` `Prod.instDecidableLE` `Preorder.toLE`	—	`left_inv_eq_right_inv` `zeta_prod_zeta` `prod_mul_prod'` `Commute.mul_mul_mul_comm` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `ite_mul` `one_mul` `MulZeroClass.zero_mul` `mu_mul_zeta` `one_prod_one` `zeta_mul_mu`
`mu_self` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Preorder.toLE` `instFunLike` `mu`	—	`mu_apply`
`mu_toDual` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `OrderDual` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Preorder.toLE` `OrderDual.instPreorder` `PartialOrder.toPreorder` `instFunLike` `mu` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `OrderDual.instLocallyFiniteOrder` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	`apply_eq_zero_of_not_le` `ext` `Finset.sum_congr` `mul_boole` `Finset.mem_Icc` `Finset.Icc_orderDual_def` `Finset.sum_map` `sum_Icc_mu_left` `EquivLike.toEmbeddingLike` `mul_assoc` `zeta_mul_mu` `mul_one` `mu_mul_zeta`
`mul_apply` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Preorder.toLE` `instFunLike` `instMul` `Finset.sum` `Finset.Icc`	—	—
`neg_apply` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `instFunLike` `instNeg` `NegZeroClass.toNeg`	—	—
`one_apply` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `Preorder.toLE` `instFunLike` `instOne`	—	—
`one_prod_one` 📖	mathematical	—	`prod` `IncidenceAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Preorder.toLE` `instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Prod.instLE_mathlib` `Prod.instPreorder`	—	`ext` `mul_ite` `mul_one` `MulZeroClass.mul_zero`
`prod_apply` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Prod.instLE_mathlib` `Preorder.toLE` `instFunLike` `prod` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`prod_mk` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Prod.instLE_mathlib` `Preorder.toLE` `instFunLike` `prod` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`prod_mul_prod` 📖	mathematical	—	`IncidenceAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `CommRing.toRing` `Prod.instLE_mathlib` `Preorder.toLE` `instMul` `Prod.instPreorder` `Prod.instLocallyFiniteOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `prod`	—	`prod_mul_prod'` `mul_mul_mul_comm`
`prod_mul_prod'` 📖	mathematical	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DFunLike.coe` `IncidenceAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Preorder.toLE` `instFunLike`	`Prod.instLE_mathlib` `instMul` `Prod.instPreorder` `Prod.instLocallyFiniteOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `prod`	—	`ext` `Finset.sum_congr` `Finset.sum_product` `Finset.sum_mul_sum`
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Preorder.toLE` `instFunLike` `instSMul` `Finset.sum` `Finset.Icc`	—	—
`sub_apply` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `instFunLike` `instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	—
`sum_Icc_mu_left` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finset.Icc` `PartialOrder.toPreorder` `DFunLike.coe` `IncidenceAlgebra` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Preorder.toLE` `instFunLike` `mu` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`sum_Icc_mu_right` 📖	mathematical	—	`Finset.sum` `AddCommGroup.toAddCommMonoid` `Finset.Icc` `PartialOrder.toPreorder` `DFunLike.coe` `IncidenceAlgebra` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Preorder.toLE` `instFunLike` `mu`	—	`Finset.sum_congr` `Finset.Icc_self` `Finset.sum_singleton` `mu_self` `Finset.right_notMem_Ico` `Finset.Icc_eq_cons_Ico` `Finset.cons_eq_insert` `Finset.sum_insert` `mu_eq_neg_sum_Ico_of_ne` `neg_add_cancel` `Finset.sum_eq_zero` `apply_eq_zero_of_not_le` `LE.le.trans` `Finset.mem_Icc`
`toFun_eq_coe` 📖	mathematical	—	`toFun` `DFunLike.coe` `IncidenceAlgebra` `instFunLike`	—	—
`zero_apply` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `instFunLike` `instZero`	—	—
`zeta_apply` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `instFunLike` `zeta`	—	—
`zeta_mul_kappa` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Preorder.toLE` `instFunLike` `instMul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `zeta` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddMonoidWithOne.toNatCast` `Finset.card` `Finset.Icc`	—	`zeta_mul_zeta`
`zeta_mul_mu` 📖	mathematical	—	`IncidenceAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Preorder.toLE` `PartialOrder.toPreorder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `instMul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `zeta` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `mu` `instOne`	—	—
`zeta_mul_zeta` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Preorder.toLE` `instFunLike` `instMul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `zeta` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddMonoidWithOne.toNatCast` `Finset.card` `Finset.Icc`	—	`mul_apply` `Finset.card_eq_sum_ones` `Nat.cast_sum` `Nat.cast_one` `Finset.sum_congr` `zeta_of_le` `Finset.mem_Icc` `one_mul`
`zeta_of_le` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `instFunLike` `zeta`	—	—
`zeta_prod_apply` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Prod.instLE_mathlib` `Preorder.toLE` `instFunLike` `zeta` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Prod.instDecidableLE` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_ite` `mul_one` `MulZeroClass.mul_zero`
`zeta_prod_mk` 📖	mathematical	—	`DFunLike.coe` `IncidenceAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Prod.instLE_mathlib` `Preorder.toLE` `instFunLike` `zeta` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Prod.instDecidableLE` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`zeta_prod_apply`
`zeta_prod_zeta` 📖	mathematical	—	`prod` `zeta` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Preorder.toLE` `Prod.instLE_mathlib` `Prod.instDecidableLE`	—	`ext` `mul_one`

(root)

Definitions

Name	Category	Theorems
`IncidenceAlgebra` 📖	CompData	42 math math: `IncidenceAlgebra.prod_mk`, `IncidenceAlgebra.constSMul_apply`, `IncidenceAlgebra.coe_constSMul`, `IncidenceAlgebra.zeta_mul_kappa`, `IncidenceAlgebra.moebius_inversion_top`, `IncidenceAlgebra.coe_sub`, `IncidenceAlgebra.one_apply`, `IncidenceAlgebra.zeta_of_le`, `IncidenceAlgebra.zeta_mul_zeta`, `IncidenceAlgebra.instIsScalarTower`, `IncidenceAlgebra.neg_apply`, `IncidenceAlgebra.mul_apply`, `IncidenceAlgebra.coe_zero`, `IncidenceAlgebra.moebius_inversion_bot`, `IncidenceAlgebra.apply_eq_zero_of_not_le`, `IncidenceAlgebra.add_apply`, `IncidenceAlgebra.mu_apply`, `IncidenceAlgebra.mu_ofDual`, `IncidenceAlgebra.smul_apply`, `IncidenceAlgebra.coe_inj`, `IncidenceAlgebra.coe_add`, `IncidenceAlgebra.prod_apply`, `IncidenceAlgebra.coe_neg`, `IncidenceAlgebra.sum_Icc_mu_left`, `IncidenceAlgebra.zero_apply`, `IncidenceAlgebra.zeta_prod_apply`, `IncidenceAlgebra.sum_Icc_mu_right`, `IncidenceAlgebra.mu_eq_neg_sum_Ioc_of_ne`, `IncidenceAlgebra.one_prod_one`, `IncidenceAlgebra.mu_mul_zeta`, `IncidenceAlgebra.zeta_mul_mu`, `IncidenceAlgebra.zeta_apply`, `IncidenceAlgebra.toFun_eq_coe`, `IncidenceAlgebra.lambda_apply`, `IncidenceAlgebra.sub_apply`, `IncidenceAlgebra.mu_eq_neg_sum_Ico_of_ne`, `IncidenceAlgebra.coe_mk`, `IncidenceAlgebra.mu_toDual`, `IncidenceAlgebra.ext_iff`, `IncidenceAlgebra.prod_mul_prod`, `IncidenceAlgebra.mu_self`, `IncidenceAlgebra.zeta_prod_mk`

---

← Back to Index