ETransform

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

Statistics

Metric	Count
Definitions addDysonETransform, addETransformLeft, addETransformRight, mulDysonETransform, mulETransformLeft, mulETransformRight	6
Theorems card, card, card, subset, vadd_finset_snd_subset_fst, addDysonETransform_fst, addDysonETransform_idem, addDysonETransform_snd, card, fst_add_snd_subset, addETransformLeft_fst, addETransformLeft_neg, addETransformLeft_snd, addETransformLeft_zero, card, fst_add_snd_subset, addETransformRight_fst, addETransformRight_neg, addETransformRight_snd, addETransformRight_zero, card, smul_finset_snd_subset_fst, subset, mulDysonETransform_fst, mulDysonETransform_idem, mulDysonETransform_snd, card, fst_mul_snd_subset, mulETransformLeft_fst, mulETransformLeft_inv, mulETransformLeft_one, mulETransformLeft_snd, card, fst_mul_snd_subset, mulETransformRight_fst, mulETransformRight_inv, mulETransformRight_one, mulETransformRight_snd	38
Total	44

Finset

Definitions

Name	Category	Theorems
addDysonETransform 📖	CompOp	6 math math: addDysonETransform.subset, addDysonETransform.card, addDysonETransform_snd, addDysonETransform_fst, addDysonETransform.vadd_finset_snd_subset_fst, addDysonETransform_idem
addETransformLeft 📖	CompOp	9 math math: addETransformLeft_neg, addETransformLeft.fst_add_snd_subset, addETransformLeft_zero, addETransformRight_neg, addETransformLeft_snd, addETransformLeft_fst, AddETransform.card, addETransformLeft.card, addETransformRight.card
addETransformRight 📖	CompOp	9 math math: addETransformRight.fst_add_snd_subset, addETransformLeft_neg, addETransformRight_snd, addETransformRight_neg, addETransformRight_zero, AddETransform.card, addETransformLeft.card, addETransformRight_fst, addETransformRight.card
mulDysonETransform 📖	CompOp	6 math math: mulDysonETransform_snd, mulDysonETransform.card, mulDysonETransform.subset, mulDysonETransform_fst, mulDysonETransform.smul_finset_snd_subset_fst, mulDysonETransform_idem
mulETransformLeft 📖	CompOp	9 math math: mulETransformLeft_one, mulETransformRight_inv, MulETransform.card, mulETransformLeft.card, mulETransformLeft_inv, mulETransformRight.card, mulETransformLeft_snd, mulETransformLeft_fst, mulETransformLeft.fst_mul_snd_subset
mulETransformRight 📖	CompOp	9 math math: mulETransformRight_one, mulETransformRight_inv, MulETransform.card, mulETransformLeft.card, mulETransformRight_fst, mulETransformRight.fst_mul_snd_subset, mulETransformLeft_inv, mulETransformRight_snd, mulETransformRight.card

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addDysonETransform_fst 📖	mathematical	—	Finset addDysonETransform instUnion HVAdd.hVAdd instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddMonoid.toAddAction	—	—
addDysonETransform_idem 📖	mathematical	—	addDysonETransform	—	vadd_finset_inter vadd_neg_vadd inter_comm union_eq_left inter_subset_union vadd_finset_union neg_vadd_vadd union_comm inter_eq_left
addDysonETransform_snd 📖	mathematical	—	Finset addDysonETransform instInter HVAdd.hVAdd instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddMonoid.toAddAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
addETransformLeft_fst 📖	mathematical	—	Finset addETransformLeft instInter HVAdd.hVAdd AddOpposite instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddOpposite.instAddMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toOppositeAddAction AddOpposite.op	—	—
addETransformLeft_neg 📖	mathematical	—	addETransformLeft AddCommGroup.toAddGroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Finset addETransformRight	—	IsCentralVAdd.op_vadd_eq_vadd isCentralVAdd AddCommSemigroup.isCentralVAdd neg_neg
addETransformLeft_snd 📖	mathematical	—	Finset addETransformLeft instUnion HVAdd.hVAdd instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	—
addETransformLeft_zero 📖	mathematical	—	addETransformLeft NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	zero_vadd inter_self neg_zero union_idempotent
addETransformRight_fst 📖	mathematical	—	Finset addETransformRight instUnion HVAdd.hVAdd AddOpposite instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddOpposite.instAddMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toOppositeAddAction AddOpposite.op	—	—
addETransformRight_neg 📖	mathematical	—	addETransformRight AddCommGroup.toAddGroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Finset addETransformLeft	—	IsCentralVAdd.op_vadd_eq_vadd isCentralVAdd AddCommSemigroup.isCentralVAdd neg_neg
addETransformRight_snd 📖	mathematical	—	Finset addETransformRight instInter HVAdd.hVAdd instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	—
addETransformRight_zero 📖	mathematical	—	addETransformRight NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	zero_vadd union_idempotent neg_zero inter_self
mulDysonETransform_fst 📖	mathematical	—	Finset mulDysonETransform instUnion smulFinset SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MulAction.toSemigroupAction Monoid.toMulAction	—	—
mulDysonETransform_idem 📖	mathematical	—	mulDysonETransform	—	smul_finset_inter smul_inv_smul inter_comm union_eq_left inter_subset_union smul_finset_union inv_smul_smul union_comm inter_eq_left
mulDysonETransform_snd 📖	mathematical	—	Finset mulDysonETransform instInter smulFinset SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MulAction.toSemigroupAction Monoid.toMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	—
mulETransformLeft_fst 📖	mathematical	—	Finset mulETransformLeft instInter MulOpposite smulFinset SemigroupAction.toSMul Monoid.toSemigroup MulOpposite.instMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toOppositeMulAction MulOpposite.op	—	—
mulETransformLeft_inv 📖	mathematical	—	mulETransformLeft CommGroup.toGroup InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid Finset mulETransformRight	—	IsCentralScalar.op_smul_eq_smul isCentralScalar CommSemigroup.isCentralScalar inv_inv
mulETransformLeft_one 📖	mathematical	—	mulETransformLeft InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	one_smul inter_self inv_one union_idempotent
mulETransformLeft_snd 📖	mathematical	—	Finset mulETransformLeft instUnion smulFinset SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
mulETransformRight_fst 📖	mathematical	—	Finset mulETransformRight instUnion MulOpposite smulFinset SemigroupAction.toSMul Monoid.toSemigroup MulOpposite.instMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toOppositeMulAction MulOpposite.op	—	—
mulETransformRight_inv 📖	mathematical	—	mulETransformRight CommGroup.toGroup InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid Finset mulETransformLeft	—	IsCentralScalar.op_smul_eq_smul isCentralScalar CommSemigroup.isCentralScalar inv_inv
mulETransformRight_one 📖	mathematical	—	mulETransformRight InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	one_smul union_idempotent inv_one inter_self
mulETransformRight_snd 📖	mathematical	—	Finset mulETransformRight instInter smulFinset SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—

Finset.AddETransform

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card 📖	mathematical	—	Finset.card Finset Finset.addETransformLeft Finset.addETransformRight	—	add_add_add_comm Finset.addETransformLeft.card Finset.addETransformRight.card mul_add Distrib.leftDistribClass Nat.instAtLeastTwoHAddOfNat two_mul

Finset.MulETransform

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card 📖	mathematical	—	Finset.card Finset Finset.mulETransformLeft Finset.mulETransformRight	—	add_add_add_comm Finset.mulETransformLeft.card Finset.mulETransformRight.card mul_add Distrib.leftDistribClass Nat.instAtLeastTwoHAddOfNat two_mul

Finset.addDysonETransform

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card 📖	mathematical	—	Finset.card Finset Finset.addDysonETransform	—	Finset.card_vadd_finset Finset.vadd_finset_inter vadd_neg_vadd Finset.inter_comm Finset.card_union_add_card_inter
subset 📖	mathematical	—	Finset Finset.instHasSubset Finset.add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Finset.addDysonETransform	—	HasSubset.Subset.trans Finset.instIsTransSubset Finset.union_add_inter_subset_union Finset.union_subset Finset.Subset.rfl add_vadd_comm Finset.vaddCommClass_finset' vaddCommClass_self vadd_add_assoc Finset.vaddAssocClass' VAddAssocClass.left neg_vadd_vadd add_comm subset_refl Finset.instReflSubset
vadd_finset_snd_subset_fst 📖	mathematical	—	Finset Finset.instHasSubset HVAdd.hVAdd instHVAdd Finset.vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddMonoid.toAddAction Finset.addDysonETransform	—	Finset.vadd_finset_inter vadd_neg_vadd Finset.inter_comm Finset.inter_subset_union

Finset.addETransformLeft

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card 📖	mathematical	—	Finset.card Finset Finset.addETransformLeft Finset.addETransformRight	—	Finset.card_inter_add_card_union Finset.card_vadd_finset Nat.instAtLeastTwoHAddOfNat two_mul
fst_add_snd_subset 📖	mathematical	—	Finset Finset.instHasSubset Finset.add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Finset.addETransformLeft	—	HasSubset.Subset.trans Finset.instIsTransSubset Finset.inter_add_union_subset_union Finset.union_subset Finset.Subset.rfl Finset.op_vadd_finset_add_eq_add_vadd_finset vadd_neg_vadd subset_refl Finset.instReflSubset

Finset.addETransformRight

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card 📖	mathematical	—	Finset.card Finset Finset.addETransformLeft Finset.addETransformRight	—	Finset.card_union_add_card_inter Finset.card_vadd_finset Nat.instAtLeastTwoHAddOfNat two_mul
fst_add_snd_subset 📖	mathematical	—	Finset Finset.instHasSubset Finset.add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Finset.addETransformRight	—	HasSubset.Subset.trans Finset.instIsTransSubset Finset.union_add_inter_subset_union Finset.union_subset Finset.Subset.rfl Finset.op_vadd_finset_add_eq_add_vadd_finset vadd_neg_vadd subset_refl Finset.instReflSubset

Finset.mulDysonETransform

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card 📖	mathematical	—	Finset.card Finset Finset.mulDysonETransform	—	Finset.card_smul_finset Finset.smul_finset_inter smul_inv_smul Finset.inter_comm Finset.card_union_add_card_inter
smul_finset_snd_subset_fst 📖	mathematical	—	Finset Finset.instHasSubset Finset.smulFinset SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MulAction.toSemigroupAction Monoid.toMulAction Finset.mulDysonETransform	—	Finset.smul_finset_inter smul_inv_smul Finset.inter_comm Finset.inter_subset_union
subset 📖	mathematical	—	Finset Finset.instHasSubset Finset.mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Finset.mulDysonETransform	—	HasSubset.Subset.trans Finset.instIsTransSubset Finset.union_mul_inter_subset_union Finset.union_subset Finset.Subset.rfl mul_smul_comm Finset.smulCommClass_finset' smulCommClass_self smul_mul_assoc Finset.isScalarTower' IsScalarTower.left inv_smul_smul mul_comm subset_refl Finset.instReflSubset

Finset.mulETransformLeft

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card 📖	mathematical	—	Finset.card Finset Finset.mulETransformLeft Finset.mulETransformRight	—	Finset.card_inter_add_card_union Finset.card_smul_finset Nat.instAtLeastTwoHAddOfNat two_mul
fst_mul_snd_subset 📖	mathematical	—	Finset Finset.instHasSubset Finset.mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Finset.mulETransformLeft	—	HasSubset.Subset.trans Finset.instIsTransSubset Finset.inter_mul_union_subset_union Finset.union_subset Finset.Subset.rfl Finset.op_smul_finset_mul_eq_mul_smul_finset smul_inv_smul subset_refl Finset.instReflSubset

Finset.mulETransformRight

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card 📖	mathematical	—	Finset.card Finset Finset.mulETransformLeft Finset.mulETransformRight	—	Finset.card_union_add_card_inter Finset.card_smul_finset Nat.instAtLeastTwoHAddOfNat two_mul
fst_mul_snd_subset 📖	mathematical	—	Finset Finset.instHasSubset Finset.mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Finset.mulETransformRight	—	HasSubset.Subset.trans Finset.instIsTransSubset Finset.union_mul_inter_subset_union Finset.union_subset Finset.Subset.rfl Finset.op_smul_finset_mul_eq_mul_smul_finset smul_inv_smul subset_refl Finset.instReflSubset

---

← Back to Index