Finset

📁 Source: Mathlib/Algebra/Group/Action/Pointwise/Finset.lean

Statistics

Metric	Count
Definitions addAction, addActionFinset, mulAction, mulActionFinset, decidablePred_mem_vadd_set	5
Theorems add_mem_vadd_finset_iff, add_singleton, add_subset_iff_left, add_subset_iff_right, biUnion_op_smul_finset, biUnion_op_vadd_finset, card_dvd_card_add_left, card_dvd_card_add_right, card_dvd_card_mul_left, card_dvd_card_mul_right, card_dvd_card_smul_right, card_dvd_card_vadd_right, card_smul_finset, card_vadd_finset, image_smul_distrib, image_vadd_distrib, inv_op_smul_finset_distrib, inv_smul_finset_distrib, inv_smul_mem_iff, isCentralScalar, isCentralVAdd, isScalarTower, isScalarTower', isScalarTower'', mem_inv_smul_finset_iff, mem_neg_vadd_finset_iff, mul_mem_smul_finset_iff, mul_singleton, mul_subset_iff_left, mul_subset_iff_right, neg_op_vadd_finset_distrib, neg_vadd_finset_distrib, neg_vadd_mem_iff, op_smul_finset_mul_eq_mul_smul_finset, op_smul_finset_subset_mul, op_vadd_finset_add_eq_add_vadd_finset, op_vadd_finset_subset_add, pairwiseDisjoint_smul_iff, pairwiseDisjoint_vadd_iff, singleton_add, singleton_mul, smulCommClass, smulCommClass_finset, smulCommClass_finset', smulCommClass_finset'', smul_finset_eq_univ, smul_finset_inter, smul_finset_sdiff, smul_finset_subset_iff, smul_finset_subset_mul, smul_finset_subset_smul_finset_iff, smul_finset_symmDiff, smul_finset_univ, smul_mem_smul_finset_iff, smul_univ, subset_smul_finset_iff, subset_vadd_finset_iff, vaddAssocClass, vaddAssocClass', vaddAssocClass'', vaddCommClass, vaddCommClass_finset, vaddCommClass_finset', vaddCommClass_finset'', vadd_finset_eq_univ, vadd_finset_inter, vadd_finset_sdiff, vadd_finset_subset_add, vadd_finset_subset_iff, vadd_finset_subset_vadd_finset_iff, vadd_finset_symmDiff, vadd_finset_univ, vadd_mem_vadd_finset_iff, vadd_univ, piFinset_smul, piFinset_smul_finset, piFinset_vadd, piFinset_vadd_finset	78
Total	83

Finset

Definitions

Name	Category	Theorems
addAction 📖	CompOp	—
addActionFinset 📖	CompOp	10 math math: op_vadd_stabilizer_of_no_doubling, AddAction.stabilizer_finset_univ, AddAction.stabilizer_finset_singleton, AddAction.mem_stabilizer_finset', AddAction.mem_stabilizer_finset_iff_subset_vadd_finset, AddAction.stabilizer_coe_finset, vadd_stabilizer_of_no_doubling, AddAction.mem_stabilizer_finset, AddAction.stabilizer_finset_empty, AddAction.mem_stabilizer_finset_iff_vadd_finset_subset
mulAction 📖	CompOp	—
mulActionFinset 📖	CompOp	10 math math: MulAction.stabilizer_finset_univ, MulAction.mem_stabilizer_finset, MulAction.stabilizer_finset_empty, MulAction.stabilizer_finset_singleton, MulAction.mem_stabilizer_finset_iff_smul_finset_subset, op_smul_stabilizer_of_no_doubling, MulAction.mem_stabilizer_finset', MulAction.stabilizer_coe_finset, smul_stabilizer_of_no_doubling, MulAction.mem_stabilizer_finset_iff_subset_smul_finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_mem_vadd_finset_iff 📖	mathematical	—	Finset instMembership HVAdd.hVAdd instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	vadd_mem_vadd_finset_iff
add_singleton 📖	mathematical	—	Finset add instSingleton HVAdd.hVAdd AddOpposite instHVAdd vaddFinset Add.toVAddAddOpposite AddOpposite.op	—	image₂_singleton_right
add_subset_iff_left 📖	mathematical	—	Finset instHasSubset add HVAdd.hVAdd instHVAdd vaddFinset Add.toVAdd	—	image₂_subset_iff_left
add_subset_iff_right 📖	mathematical	—	Finset instHasSubset add HVAdd.hVAdd AddOpposite instHVAdd vaddFinset Add.toVAddAddOpposite AddOpposite.op	—	image₂_subset_iff_right
biUnion_op_smul_finset 📖	mathematical	—	biUnion MulOpposite Finset smulFinset Mul.toSMulMulOpposite MulOpposite.op mul	—	biUnion_image_right
biUnion_op_vadd_finset 📖	mathematical	—	biUnion HVAdd.hVAdd AddOpposite Finset instHVAdd vaddFinset Add.toVAddAddOpposite AddOpposite.op add	—	biUnion_image_right
card_dvd_card_add_left 📖	mathematical	Set.PairwiseDisjoint Finset partialOrder instOrderBot Set.image image AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SetLike.coe instSetLike	card add	—	card_dvd_card_image₂_left add_left_injective AddRightCancelSemigroup.toIsRightCancelAdd
card_dvd_card_add_right 📖	mathematical	Set.PairwiseDisjoint Finset partialOrder instOrderBot Set.image HVAdd.hVAdd instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction SetLike.coe instSetLike	card add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	card_dvd_card_image₂_right add_right_injective AddLeftCancelSemigroup.toIsLeftCancelAdd
card_dvd_card_mul_left 📖	mathematical	Set.PairwiseDisjoint Finset partialOrder instOrderBot Set.image image MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SetLike.coe instSetLike	card mul	—	card_dvd_card_image₂_left mul_left_injective RightCancelSemigroup.toIsRightCancelMul
card_dvd_card_mul_right 📖	mathematical	Set.PairwiseDisjoint Finset partialOrder instOrderBot Set.image smulFinset SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction SetLike.coe instSetLike	card mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	card_dvd_card_image₂_right mul_right_injective LeftCancelSemigroup.toIsLeftCancelMul
card_dvd_card_smul_right 📖	mathematical	Set.PairwiseDisjoint Finset partialOrder instOrderBot Set.image smulFinset SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction SetLike.coe instSetLike	card smul	—	card_dvd_card_image₂_right MulAction.injective
card_dvd_card_vadd_right 📖	mathematical	Set.PairwiseDisjoint Finset partialOrder instOrderBot Set.image HVAdd.hVAdd instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction SetLike.coe instSetLike	card vadd	—	card_dvd_card_image₂_right AddAction.injective
card_smul_finset 📖	mathematical	—	card Finset smulFinset SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	card_image_of_injective MulAction.injective
card_vadd_finset 📖	mathematical	—	card HVAdd.hVAdd Finset instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	—	card_image_of_injective AddAction.injective
image_smul_distrib 📖	mathematical	—	image DFunLike.coe Finset smulFinset	—	image_comm map_mul
image_vadd_distrib 📖	mathematical	—	image DFunLike.coe HVAdd.hVAdd Finset instHVAdd vaddFinset Add.toVAdd	—	image_comm map_add
inv_op_smul_finset_distrib 📖	mathematical	—	Finset inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid MulOpposite smulFinset SemigroupAction.toSMul Monoid.toSemigroup MulOpposite.instMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toOppositeMulAction MulOpposite.op Monoid.toMulAction	—	ext inv_inv mul_inv_rev
inv_smul_finset_distrib 📖	mathematical	—	Finset inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid smulFinset SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction MulOpposite MulOpposite.instMonoid Monoid.toOppositeMulAction MulOpposite.op	—	ext inv_inv mul_inv_rev
inv_smul_mem_iff 📖	mathematical	—	Finset instMembership SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid smulFinset	—	smul_mem_smul_finset_iff smul_inv_smul
isCentralScalar 📖	mathematical	—	IsCentralScalar Finset smulFinset MulOpposite	—	coe_injective coe_smul_finset IsCentralScalar.op_smul_eq_smul Set.isCentralScalar
isCentralVAdd 📖	mathematical	—	IsCentralVAdd Finset vaddFinset AddOpposite	—	coe_injective coe_vadd_finset IsCentralVAdd.op_vadd_eq_vadd Set.isCentralVAdd
isScalarTower 📖	mathematical	—	IsScalarTower Finset smulFinset	—	smul_assoc image_image
isScalarTower' 📖	mathematical	—	IsScalarTower Finset smulFinset smul	—	coe_injective coe_smul coe_smul_finset smul_assoc Set.isScalarTower'
isScalarTower'' 📖	mathematical	—	IsScalarTower Finset smul	—	coe_injective coe_smul smul_assoc Set.isScalarTower''
mem_inv_smul_finset_iff 📖	mathematical	—	Finset instMembership smulFinset SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	smul_mem_smul_finset_iff smul_inv_smul
mem_neg_vadd_finset_iff 📖	mathematical	—	Finset instMembership HVAdd.hVAdd instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	vadd_mem_vadd_finset_iff vadd_neg_vadd
mul_mem_smul_finset_iff 📖	mathematical	—	Finset instMembership smulFinset SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	smul_mem_smul_finset_iff
mul_singleton 📖	mathematical	—	Finset mul instSingleton MulOpposite smulFinset Mul.toSMulMulOpposite MulOpposite.op	—	image₂_singleton_right
mul_subset_iff_left 📖	mathematical	—	Finset instHasSubset mul smulFinset	—	image₂_subset_iff_left
mul_subset_iff_right 📖	mathematical	—	Finset instHasSubset mul MulOpposite smulFinset Mul.toSMulMulOpposite MulOpposite.op	—	image₂_subset_iff_right
neg_op_vadd_finset_distrib 📖	mathematical	—	Finset neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid HVAdd.hVAdd AddOpposite instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddOpposite.instAddMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toOppositeAddAction AddOpposite.op AddMonoid.toAddAction	—	ext mem_neg' neg_vadd_mem_iff neg_neg neg_add_rev
neg_vadd_finset_distrib 📖	mathematical	—	Finset neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid HVAdd.hVAdd instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction AddOpposite AddOpposite.instAddMonoid AddMonoid.toOppositeAddAction AddOpposite.op	—	ext mem_neg' neg_vadd_mem_iff neg_neg neg_add_rev
neg_vadd_mem_iff 📖	mathematical	—	Finset instMembership HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid vaddFinset	—	vadd_mem_vadd_finset_iff vadd_neg_vadd
op_smul_finset_mul_eq_mul_smul_finset 📖	mathematical	—	Finset mul Semigroup.toMul MulOpposite smulFinset Mul.toSMulMulOpposite MulOpposite.op	—	op_smul_finset_smul_eq_smul_smul_finset mul_assoc
op_smul_finset_subset_mul 📖	mathematical	Finset instMembership	instHasSubset MulOpposite smulFinset Mul.toSMulMulOpposite MulOpposite.op mul	—	image_subset_image₂_left
op_vadd_finset_add_eq_add_vadd_finset 📖	mathematical	—	Finset add AddSemigroup.toAdd HVAdd.hVAdd AddOpposite instHVAdd vaddFinset Add.toVAddAddOpposite AddOpposite.op Add.toVAdd	—	op_vadd_finset_vadd_eq_vadd_vadd_finset add_assoc
op_vadd_finset_subset_add 📖	mathematical	Finset instMembership	instHasSubset HVAdd.hVAdd AddOpposite instHVAdd vaddFinset Add.toVAddAddOpposite AddOpposite.op add	—	image_subset_image₂_left
pairwiseDisjoint_smul_iff 📖	mathematical	—	Set.PairwiseDisjoint Finset partialOrder instOrderBot smulFinset Set.InjOn SProd.sprod Set Set.instSProd SetLike.coe instSetLike	—	coe_smul_finset
pairwiseDisjoint_vadd_iff 📖	mathematical	—	Set.PairwiseDisjoint Finset partialOrder instOrderBot HVAdd.hVAdd instHVAdd vaddFinset Add.toVAdd Set.InjOn SProd.sprod Set Set.instSProd SetLike.coe instSetLike	—	pairwiseDisjoint_coe coe_vadd_finset Set.pairwiseDisjoint_vadd_iff
singleton_add 📖	mathematical	—	Finset add instSingleton HVAdd.hVAdd instHVAdd vaddFinset Add.toVAdd	—	image₂_singleton_left
singleton_mul 📖	mathematical	—	Finset mul instSingleton smulFinset	—	image₂_singleton_left
smulCommClass 📖	mathematical	—	SMulCommClass Finset smul	—	coe_injective coe_smul SMulCommClass.smul_comm Set.smulCommClass
smulCommClass_finset 📖	mathematical	—	SMulCommClass Finset smulFinset	—	Function.Commute.finset_image SMulCommClass.smul_comm
smulCommClass_finset' 📖	mathematical	—	SMulCommClass Finset smulFinset smul	—	coe_injective coe_smul_finset coe_smul SMulCommClass.smul_comm Set.smulCommClass_set'
smulCommClass_finset'' 📖	mathematical	—	SMulCommClass Finset smul smulFinset	—	SMulCommClass.symm smulCommClass_finset'
smul_finset_eq_univ 📖	mathematical	—	Finset smulFinset SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction univ	—	smul_eq_iff_eq_inv_smul smul_finset_univ
smul_finset_inter 📖	mathematical	—	Finset smulFinset SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instInter	—	image_inter MulAction.injective
smul_finset_sdiff 📖	mathematical	—	Finset smulFinset SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instSDiff	—	image_sdiff MulAction.injective
smul_finset_subset_iff 📖	mathematical	—	Finset instHasSubset smulFinset SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	coe_smul_finset Set.smul_set_subset_iff_subset_inv_smul_set
smul_finset_subset_mul 📖	mathematical	Finset instMembership	instHasSubset smulFinset mul	—	image_subset_image₂_right
smul_finset_subset_smul_finset_iff 📖	mathematical	—	Finset instHasSubset smulFinset SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	image_subset_image_iff MulAction.injective
smul_finset_symmDiff 📖	mathematical	—	Finset smulFinset SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup instLattice instSDiff	—	image_symmDiff MulAction.injective
smul_finset_univ 📖	mathematical	—	Finset smulFinset SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction univ	—	image_univ_of_surjective MulAction.surjective
smul_mem_smul_finset_iff 📖	mathematical	—	Finset instMembership smulFinset SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	Function.Injective.mem_finset_image MulAction.injective
smul_univ 📖	mathematical	Nonempty	Finset smul SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction univ	—	coe_injective coe_smul coe_univ Set.smul_univ
subset_smul_finset_iff 📖	mathematical	—	Finset instHasSubset smulFinset SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	coe_smul_finset Set.subset_smul_set_iff
subset_vadd_finset_iff 📖	mathematical	—	Finset instHasSubset HVAdd.hVAdd instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	coe_subset coe_vadd_finset Set.subset_vadd_set_iff
vaddAssocClass 📖	mathematical	—	VAddAssocClass Finset vaddFinset	—	vadd_assoc image_image
vaddAssocClass' 📖	mathematical	—	VAddAssocClass Finset vaddFinset vadd	—	coe_injective coe_vadd coe_vadd_finset vadd_assoc Set.vaddAssocClass'
vaddAssocClass'' 📖	mathematical	—	VAddAssocClass Finset vadd	—	coe_injective coe_vadd vadd_assoc Set.vaddAssocClass''
vaddCommClass 📖	mathematical	—	VAddCommClass Finset vadd	—	coe_injective coe_vadd VAddCommClass.vadd_comm Set.vaddCommClass
vaddCommClass_finset 📖	mathematical	—	VAddCommClass Finset vaddFinset	—	Function.Commute.finset_image VAddCommClass.vadd_comm
vaddCommClass_finset' 📖	mathematical	—	VAddCommClass Finset vaddFinset vadd	—	coe_injective coe_vadd_finset coe_vadd VAddCommClass.vadd_comm Set.vaddCommClass_set'
vaddCommClass_finset'' 📖	mathematical	—	VAddCommClass Finset vadd vaddFinset	—	VAddCommClass.symm vaddCommClass_finset'
vadd_finset_eq_univ 📖	mathematical	—	HVAdd.hVAdd Finset instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction univ	—	vadd_eq_iff_eq_neg_vadd vadd_finset_univ
vadd_finset_inter 📖	mathematical	—	HVAdd.hVAdd Finset instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction instInter	—	image_inter AddAction.injective
vadd_finset_sdiff 📖	mathematical	—	HVAdd.hVAdd Finset instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction instSDiff	—	image_sdiff AddAction.injective
vadd_finset_subset_add 📖	mathematical	Finset instMembership	instHasSubset HVAdd.hVAdd instHVAdd vaddFinset Add.toVAdd add	—	image_subset_image₂_right
vadd_finset_subset_iff 📖	mathematical	—	Finset instHasSubset HVAdd.hVAdd instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	coe_subset coe_vadd_finset Set.vadd_set_subset_iff_subset_neg_vadd_set
vadd_finset_subset_vadd_finset_iff 📖	mathematical	—	Finset instHasSubset HVAdd.hVAdd instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	—	image_subset_image_iff AddAction.injective
vadd_finset_symmDiff 📖	mathematical	—	HVAdd.hVAdd Finset instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup instLattice instSDiff	—	image_symmDiff AddAction.injective
vadd_finset_univ 📖	mathematical	—	HVAdd.hVAdd Finset instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction univ	—	image_univ_of_surjective AddAction.surjective
vadd_mem_vadd_finset_iff 📖	mathematical	—	Finset instMembership HVAdd.hVAdd instHVAdd vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	—	Function.Injective.mem_finset_image AddAction.injective
vadd_univ 📖	mathematical	Nonempty	HVAdd.hVAdd Finset instHVAdd vadd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction univ	—	coe_injective coe_vadd coe_univ Set.vadd_univ

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
piFinset_smul 📖	mathematical	—	piFinset Finset Finset.smul decidablePiFintype Pi.smul'	—	piFinset_image₂
piFinset_smul_finset 📖	mathematical	—	piFinset Finset Finset.smulFinset decidablePiFintype Pi.smul'	—	piFinset_image
piFinset_vadd 📖	mathematical	—	piFinset HVAdd.hVAdd Finset instHVAdd Finset.vadd decidablePiFintype Pi.vadd'	—	piFinset_image₂
piFinset_vadd_finset 📖	mathematical	—	piFinset HVAdd.hVAdd Finset instHVAdd Finset.vaddFinset decidablePiFintype Pi.vadd'	—	piFinset_image

Nat

Definitions

Name	Category	Theorems
decidablePred_mem_vadd_set 📖	CompOp	—

---

← Back to Index