Commit 2024-11-11 17:57 fa330e6e

View on Github →

feat: Incidence algebras (#8900) Define incidence algebras From LeanCamCombi

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean

added theorem IncidenceAlgebra.add_apply

added theorem IncidenceAlgebra.apply_eq_zero_of_not_le

added theorem IncidenceAlgebra.coe_add

added theorem IncidenceAlgebra.coe_constSMul

added theorem IncidenceAlgebra.coe_inj

added theorem IncidenceAlgebra.coe_mk

added theorem IncidenceAlgebra.coe_neg

added theorem IncidenceAlgebra.coe_sub

added theorem IncidenceAlgebra.coe_zero

added theorem IncidenceAlgebra.constSMul_apply

added theorem IncidenceAlgebra.ext

added def IncidenceAlgebra.lambda

added theorem IncidenceAlgebra.le_of_ne_zero

added theorem IncidenceAlgebra.mk_coe

added theorem IncidenceAlgebra.moebius_inversion_bot

added theorem IncidenceAlgebra.moebius_inversion_top

added def IncidenceAlgebra.mu

added theorem IncidenceAlgebra.mu_apply

added theorem IncidenceAlgebra.mu_eq_neg_sum_Ico_of_ne

added theorem IncidenceAlgebra.mu_eq_neg_sum_Ioc_of_ne

added theorem IncidenceAlgebra.mu_mul_zeta

added theorem IncidenceAlgebra.mu_ofDual

added theorem IncidenceAlgebra.mu_prod_mu

added theorem IncidenceAlgebra.mu_self

added theorem IncidenceAlgebra.mu_toDual

added theorem IncidenceAlgebra.mul_apply

added theorem IncidenceAlgebra.neg_apply

added theorem IncidenceAlgebra.one_apply

added theorem IncidenceAlgebra.one_prod_one

added theorem IncidenceAlgebra.prod_apply

added theorem IncidenceAlgebra.prod_mk

added theorem IncidenceAlgebra.prod_mul_prod'

added theorem IncidenceAlgebra.prod_mul_prod

added theorem IncidenceAlgebra.smul_apply

added theorem IncidenceAlgebra.sub_apply

added theorem IncidenceAlgebra.sum_Icc_mu_left

added theorem IncidenceAlgebra.sum_Icc_mu_right

added theorem IncidenceAlgebra.toFun_eq_coe

added theorem IncidenceAlgebra.zero_apply

added def IncidenceAlgebra.zeta

added theorem IncidenceAlgebra.zeta_apply

added theorem IncidenceAlgebra.zeta_mul_kappa

added theorem IncidenceAlgebra.zeta_mul_mu

added theorem IncidenceAlgebra.zeta_mul_zeta

added theorem IncidenceAlgebra.zeta_of_le

added theorem IncidenceAlgebra.zeta_prod_apply

added theorem IncidenceAlgebra.zeta_prod_mk

added theorem IncidenceAlgebra.zeta_prod_zeta

added structure IncidenceAlgebra

Modified Mathlib/Order/Interval/Finset/Defs.lean

added theorem Icc_orderDual_def

added theorem Ici_orderDual_def

added theorem Ico_orderDual_def

added theorem Iic_orderDual_def

added theorem Iio_orderDual_def

added theorem Ioc_orderDual_def

added theorem Ioi_orderDual_def

added theorem Ioo_orderDual_def

Modified docs/references.bib