Convolution

📁 Source: Mathlib/Combinatorics/Additive/Convolution.lean

Statistics

Metric	Count
Definitions addConvolution, convolution	2
Theorems addConvolution_eq_zero, addConvolution_le_card_left, addConvolution_le_card_right, addConvolution_ne_zero, addConvolution_neg, addConvolution_op_vadd_eq_addConvolution_add_neg, addConvolution_pos, card_add_neg_eq_addConvolution_neg, card_inter_smul, card_inter_vadd, card_mul_inv_eq_convolution_inv, card_smul_inter, card_smul_inter_smul, card_vadd_inter, card_vadd_inter_vadd, convolution_eq_zero, convolution_inv, convolution_le_card_left, convolution_le_card_right, convolution_ne_zero, convolution_op_smul_eq_convolution_mul_inv, convolution_pos, op_smul_convolution_eq_convolution_smul, op_vadd_addConvolution_eq_addConvolution_vadd, smul_convolution_eq_convolution_inv_mul, vadd_addConvolution_eq_addConvolution_neg_add	26
Total	28

Finset

Definitions

Name	Category	Theorems
addConvolution 📖	CompOp	12 math math: addConvolution_eq_zero, vadd_addConvolution_eq_addConvolution_neg_add, card_inter_vadd, addConvolution_le_card_left, addConvolution_pos, op_vadd_addConvolution_eq_addConvolution_vadd, addConvolution_neg, card_vadd_inter, addConvolution_op_vadd_eq_addConvolution_add_neg, card_add_neg_eq_addConvolution_neg, addConvolution_le_card_right, card_vadd_inter_vadd
convolution 📖	CompOp	12 math math: card_mul_inv_eq_convolution_inv, convolution_inv, card_smul_inter, op_smul_convolution_eq_convolution_smul, convolution_le_card_left, smul_convolution_eq_convolution_inv_mul, card_inter_smul, convolution_eq_zero, card_smul_inter_smul, convolution_pos, convolution_le_card_right, convolution_op_smul_eq_convolution_mul_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addConvolution_eq_zero 📖	mathematical	—	addConvolution Finset instMembership add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	addConvolution_ne_zero
addConvolution_le_card_left 📖	mathematical	—	addConvolution card	—	neg_neg card_inter_vadd card_le_card inter_subset_left
addConvolution_le_card_right 📖	mathematical	—	addConvolution card	—	neg_neg card_vadd_inter card_neg card_le_card inter_subset_right
addConvolution_ne_zero 📖	mathematical	—	Finset instMembership add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	addConvolution_pos
addConvolution_neg 📖	mathematical	—	addConvolution NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Finset neg	—	neg_neg card_vadd_inter card_inter_vadd inter_comm
addConvolution_op_vadd_eq_addConvolution_add_neg 📖	mathematical	—	addConvolution HVAdd.hVAdd AddOpposite Finset instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddOpposite.instAddMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toOppositeAddAction AddOpposite.op AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	neg_neg neg_op_vadd_finset_distrib card_inter_vadd vadd_vadd
addConvolution_pos 📖	mathematical	—	addConvolution Finset instMembership add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	card_pos mem_filter mem_product mem_add AddLeftCancelSemigroup.toIsLeftCancelAdd
card_add_neg_eq_addConvolution_neg 📖	mathematical	—	card filter AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SProd.sprod Finset instSProd addConvolution neg	—	card_nbij' coe_filter mem_product mem_neg' neg_neg
card_inter_smul 📖	mathematical	—	card Finset instInter smulFinset SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction convolution inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	one_smul convolution.congr_simp inv_one one_mul card_smul_inter_smul
card_inter_vadd 📖	mathematical	—	card Finset instInter HVAdd.hVAdd instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction addConvolution neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	zero_vadd addConvolution.congr_simp neg_zero zero_add card_vadd_inter_vadd
card_mul_inv_eq_convolution_inv 📖	mathematical	—	card filter MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SProd.sprod Finset instSProd convolution inv	—	card_nbij' coe_filter inv_inv
card_smul_inter 📖	mathematical	—	card Finset instInter smulFinset SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction convolution inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	one_smul convolution.congr_simp mul_one card_smul_inter_smul
card_smul_inter_smul 📖	mathematical	—	card Finset instInter smulFinset SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction convolution inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	card_nbij' coe_inter coe_smul_finset coe_filter mul_inv_rev inv_inv mul_assoc mul_inv_cancel_left inv_mul_cancel_left filter.congr_simp inv_mul_cancel mul_one
card_vadd_inter 📖	mathematical	—	card Finset instInter HVAdd.hVAdd instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction addConvolution neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	zero_vadd addConvolution.congr_simp add_zero card_vadd_inter_vadd
card_vadd_inter_vadd 📖	mathematical	—	card Finset instInter HVAdd.hVAdd instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction addConvolution neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	card_nbij' coe_inter coe_vadd_finset Set.mem_inter_iff Set.mem_vadd_set_iff_neg_vadd_mem SetLike.mem_coe coe_filter mem_product mem_neg' neg_add_rev neg_neg add_assoc add_neg_cancel_left neg_add_cancel_left eq_add_neg_iff_add_eq filter.congr_simp neg_add_cancel add_zero
convolution_eq_zero 📖	mathematical	—	convolution Finset instMembership mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	—
convolution_inv 📖	mathematical	—	convolution InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Finset inv	—	inv_inv card_smul_inter card_inter_smul inter_comm
convolution_le_card_left 📖	mathematical	—	convolution card	—	inv_inv card_inter_smul card_le_card inter_subset_left
convolution_le_card_right 📖	mathematical	—	convolution card	—	inv_inv card_smul_inter card_inv card_le_card inter_subset_right
convolution_ne_zero 📖	mathematical	—	Finset instMembership mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	—
convolution_op_smul_eq_convolution_mul_inv 📖	mathematical	—	convolution MulOpposite Finset smulFinset SemigroupAction.toSMul Monoid.toSemigroup MulOpposite.instMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toOppositeMulAction MulOpposite.op MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	inv_inv inv_op_smul_finset_distrib card_inter_smul smul_smul
convolution_pos 📖	mathematical	—	convolution Finset instMembership mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	LeftCancelSemigroup.toIsLeftCancelMul
op_smul_convolution_eq_convolution_smul 📖	mathematical	—	convolution MulOpposite Finset smulFinset SemigroupAction.toSMul Monoid.toSemigroup MulOpposite.instMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toOppositeMulAction MulOpposite.op Monoid.toMulAction	—	inv_inv inv_smul_finset_distrib card_inter_smul SMulCommClass.smul_comm smulCommClass_finset SMulCommClass.opposite_mid IsScalarTower.left card_smul_finset smul_finset_inter smul_inv_smul
op_vadd_addConvolution_eq_addConvolution_vadd 📖	mathematical	—	addConvolution HVAdd.hVAdd AddOpposite Finset instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddOpposite.instAddMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toOppositeAddAction AddOpposite.op AddMonoid.toAddAction	—	neg_neg neg_vadd_finset_distrib card_inter_vadd VAddCommClass.vadd_comm vaddCommClass_finset VAddCommClass.opposite_mid VAddAssocClass.left card_vadd_finset vadd_finset_inter vadd_neg_vadd
smul_convolution_eq_convolution_inv_mul 📖	mathematical	—	convolution Finset smulFinset SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	inv_inv card_smul_inter mul_inv_rev smul_smul
vadd_addConvolution_eq_addConvolution_neg_add 📖	mathematical	—	addConvolution HVAdd.hVAdd Finset instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	neg_neg card_vadd_inter neg_add_rev vadd_vadd

---

← Back to Index