Basic

📁 Source: Mathlib/Algebra/Group/Action/Pointwise/Set/Basic.lean

Statistics

Metric	Count
Definitions addAction, addActionSet, mulAction, mulActionSet	4
Theorems add_pair, add_subset_iff_left, add_subset_iff_right, disjoint_smul_set, disjoint_smul_set_left, disjoint_smul_set_right, disjoint_vadd_set, disjoint_vadd_set_left, disjoint_vadd_set_right, exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul, exists_vadd_inter_vadd_subset_vadd_neg_add_inter_neg_add, iUnion_inv_smul, iUnion_neg_vadd, iUnion_op_smul_set, iUnion_op_vadd_set, iUnion_smul_eq_setOf_exists, iUnion_vadd_eq_setOf_exists, image_op_smul, image_op_smul_distrib, image_op_vadd, image_op_vadd_distrib, image_smul_distrib, image_vadd_distrib, inv_op_smul_set_distrib, inv_smul_set_distrib, isCentralScalar, isCentralVAdd, isScalarTower, isScalarTower', isScalarTower'', mem_invOf_smul_set, mem_inv_smul_set_iff, mem_neg_vadd_set_iff, mem_smul_set_iff_inv_smul_mem, mem_smul_set_inv, mem_vadd_set_iff_neg_vadd_mem, mem_vadd_set_neg, mul_pair, mul_subset_iff_left, mul_subset_iff_right, neg_op_vadd_set_distrib, neg_vadd_set_distrib, op_smul_inter_ne_empty_iff, op_smul_inter_nonempty_iff, op_smul_set_mul_eq_mul_smul_set, op_smul_set_subset_mul, op_vadd_inter_ne_empty_iff, op_vadd_inter_nonempty_iff, op_vadd_set_add_eq_add_vadd_set, op_vadd_set_subset_add, pair_add, pair_mul, pairwiseDisjoint_smul_iff, pairwiseDisjoint_vadd_iff, pairwise_disjoint_smul_iff, pairwise_disjoint_vadd_iff, preimage_smul, preimage_smul_inv, preimage_vadd, preimage_vadd_neg, range_add, range_mul, smulCommClass, smulCommClass_set, smulCommClass_set', smulCommClass_set'', smul_div_smul_comm, smul_graphOn, smul_graphOn_univ, smul_inter_ne_empty_iff, smul_inter_ne_empty_iff', smul_inter_nonempty_iff, smul_inter_nonempty_iff', smul_mem_smul_set_iff, smul_set_compl, smul_set_eq_univ, smul_set_iInter, smul_set_inter, smul_set_pi, smul_set_pi_of_isUnit, smul_set_prod, smul_set_sdiff, smul_set_subset_iff_subset_inv_smul_set, smul_set_subset_mul, smul_set_subset_smul_set_iff, smul_set_symmDiff, smul_set_univ, smul_univ, subset_smul_set_iff, subset_vadd_set_iff, vaddAssocClass, vaddAssocClass', vaddAssocClass'', vaddCommClass, vaddCommClass_set, vaddCommClass_set', vaddCommClass_set'', vadd_graphOn, vadd_graphOn_univ, vadd_inter_ne_empty_iff, vadd_inter_ne_empty_iff', vadd_inter_nonempty_iff, vadd_inter_nonempty_iff', vadd_mem_vadd_set_iff, vadd_set_compl, vadd_set_eq_univ, vadd_set_iInter, vadd_set_inter, vadd_set_pi, vadd_set_pi_of_isAddUnit, vadd_set_prod, vadd_set_sdiff, vadd_set_subset_add, vadd_set_subset_iff_subset_neg_vadd_set, vadd_set_subset_vadd_set_iff, vadd_set_symmDiff, vadd_set_univ, vadd_sub_vadd_comm, vadd_univ	119
Total	123

Set

Definitions

Name	Category	Theorems
addAction 📖	CompOp	—
addActionSet 📖	CompOp	36 math math: AddAction.mem_stabilizer_set_iff_subset_vadd_set, AddAction.stabilizer_addSubgroup_op, AddAction.stabilizer_inf_stabilizer_le_stabilizer_apply₂, AddAction.stabilizer_singleton, AddAction.map_stabilizer_le, AddAction.movedBy_mem_fixedBy_of_addCommute, AddAction.stabilizer_le_aestabilizer, AddAction.stabilizer_univ, AddAction.stabilizer_empty, AddAction.stabilizer_add_self, powersetCard.addAction_stabilizer_coe, AddAction.IsBlock.stabilizer_le, AddAction.stabilizer_op_addSubgroup, AddAction.fixingAddSubgroup_le_stabilizer, AddAction.stabilizer_inf_stabilizer_le_stabilizer_inter, AddAction.set_mem_fixedBy_of_movedBy_subset, AddAction.mem_stabilizer_set', AddAction.op_vadd_set_stabilizer_subset, AddAction.stabilizer_inf_stabilizer_le_stabilizer_union, AddAction.stabilizer_coe_finset, AddAction.IsBlock.orbit_stabilizer_eq, AddAction.stabilizer_addSubgroup, AddAction.stabilizer_image_coe_quotient, AddAction.set_mem_fixedBy_iff, AddAction.stabilizer_finite, AddAction.mem_stabilizer_set_iff_vadd_set_subset, AddAction.add_stabilizer_self, AddAction.set_mem_fixedBy_of_subset_fixedBy, AddAction.stabilizer_subset_sub_right, AddAction.le_stabilizer_iff_vadd_le, AddAction.mem_stabilizer_set, AddAction.stabilizer_inf_stabilizer_le_stabilizer_sdiff, AddAction.stabilizer_orbit_eq, AddAction.fixedBy_mem_fixedBy_of_addCommute, AddAction.IsBlock.ncard_block_eq_relIndex, AddAction.vadd_set_stabilizer_subset
mulAction 📖	CompOp	—
mulActionSet 📖	CompOp	65 math math: DiscreteTiling.PlacedTile.ext_iff_of_preimage, MulAction.set_mem_fixedBy_iff, Equiv.Perm.exists_mem_stabilizer_smul_eq, MulAction.stabilizer_mul_self, Equiv.Perm.exists_mem_stabilizer_isThreeCycle_of_two_lt_ncard, MulAction.le_stabilizer_iff_smul_le, MulAction.stabilizer_inf_stabilizer_le_stabilizer_sdiff, DiscreteTiling.PlacedTile.ext_iff_of_exists, MulAction.op_smul_set_stabilizer_subset, MulAction.mul_stabilizer_self, alternatingGroup.isCoatom_stabilizer_singleton, powersetCard.stabilizer_coe, MulAction.IsBlock.stabilizer_le, DiscreteTiling.PlacedTile.smul_mk_mk, stabilizer_compl, DiscreteTiling.PlacedTile.ext_iff, DiscreteTiling.Prototile.ext_iff, alternatingGroup.stabilizer.surjective_toPerm, MulAction.IsBlock.orbit_stabilizer_eq, Equiv.Perm.swap_mem_stabilizer, stabilizer_empty_eq_top, MulAction.set_mem_fixedBy_of_subset_fixedBy, MulAction.stabilizer_subgroup, MulAction.mem_stabilizer_set_iff_subset_smul_set, DiscreteTiling.PlacedTile.coe_mk_mk, MulAction.smul_set_stabilizer_subset, Equiv.Perm.stabilizer_isPreprimitive, MulAction.stabilizer_subset_div_right, MulAction.mem_stabilizer_set', MulAction.stabilizer_univ, MulAction.stabilizer_subgroup_op, MulAction.stabilizer_empty, DiscreteTiling.PlacedTile.smul_mk_coe, MulAction.stabilizer_op_subgroup, MulAction.stabilizer_le_aestabilizer, MulAction.mem_stabilizer_set, Equiv.swap_mem_stabilizer, MulAction.map_stabilizer_le, alternatingGroup.exists_mem_stabilizer_smul_eq, Equiv.Perm.exists_mem_stabilizer_isThreeCycle, MulAction.IsBlock.ncard_block_eq_relIndex, MulAction.mem_stabilizer_set_iff_smul_set_subset, alternatingGroup.stabilizer_isPreprimitive, MulAction.stabilizer_image_coe_quotient, alternatingGroup.isCoatom_stabilizer, Equiv.Perm.isCoatom_stabilizer, MulAction.set_mem_fixedBy_of_movedBy_subset, MulAction.stabilizer_orbit_eq, MulAction.stabilizer_finite, MulAction.stabilizer_inf_stabilizer_le_stabilizer_inter, MulAction.stabilizer_inf_stabilizer_le_stabilizer_apply₂, Equiv.Perm.stabilizer.surjective_toPerm, DiscreteTiling.PlacedTile.coe_mk_coe, MulAction.stabilizer_inf_stabilizer_le_stabilizer_union, Equiv.Perm.isCoatom_stabilizer_of_ncard_lt_ncard_compl, MulAction.fixingSubgroup_le_stabilizer, Equiv.Perm.moves_in, MulAction.stabilizer_singleton, MulAction.fixedBy_mem_fixedBy_of_commute, Equiv.Perm.ofSubtype_mem_stabilizer, SMul.smul_stabilizer_def, MulAction.stabilizer_coe_finset, MulAction.movedBy_mem_fixedBy_of_commute, alternatingGroup.isCoatom_stabilizer_of_ncard_lt_ncard_compl, stabilizer_univ_eq_top

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_pair 📖	mathematical	—	Set add instInsert instSingletonSet instUnion HVAdd.hVAdd AddOpposite instHVAdd vaddSet Add.toVAddAddOpposite AddOpposite.op	—	insert_eq add_union add_singleton
add_subset_iff_left 📖	mathematical	—	Set instHasSubset add HVAdd.hVAdd instHVAdd vaddSet Add.toVAdd	—	image2_subset_iff_left
add_subset_iff_right 📖	mathematical	—	Set instHasSubset add HVAdd.hVAdd AddOpposite instHVAdd vaddSet Add.toVAddAddOpposite AddOpposite.op	—	image2_subset_iff_right
disjoint_smul_set 📖	mathematical	—	Disjoint Set CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	disjoint_image_iff MulAction.injective
disjoint_smul_set_left 📖	mathematical	—	Disjoint Set CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	smul_inv_smul disjoint_smul_set
disjoint_smul_set_right 📖	mathematical	—	Disjoint Set CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	smul_inv_smul disjoint_smul_set
disjoint_vadd_set 📖	mathematical	—	Disjoint Set CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice HVAdd.hVAdd instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	—	disjoint_image_iff AddAction.injective
disjoint_vadd_set_left 📖	mathematical	—	Disjoint Set CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice HVAdd.hVAdd instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	vadd_neg_vadd disjoint_vadd_set
disjoint_vadd_set_right 📖	mathematical	—	Disjoint Set CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice HVAdd.hVAdd instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	vadd_neg_vadd disjoint_vadd_set
exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul 📖	mathematical	—	Set instHasSubset instInter smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	eq_empty_or_nonempty one_smul inter_subset_inter smul_set_subset_mul smul_set_inter smul_mul_assoc isScalarTower' IsScalarTower.left
exists_vadd_inter_vadd_subset_vadd_neg_add_inter_neg_add 📖	mathematical	—	Set instHasSubset instInter HVAdd.hVAdd instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	eq_empty_or_nonempty zero_vadd subset_inter_iff empty_subset inter_subset_inter vadd_set_subset_add mem_vadd_set_neg vadd_set_inter vadd_add_assoc vaddAssocClass' VAddAssocClass.left
iUnion_inv_smul 📖	mathematical	—	iUnion Set smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Function.Surjective.iSup_congr inv_surjective
iUnion_neg_vadd 📖	mathematical	—	iUnion HVAdd.hVAdd Set instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	Function.Surjective.iSup_congr neg_surjective
iUnion_op_smul_set 📖	mathematical	—	iUnion Set instMembership MulOpposite smulSet Mul.toSMulMulOpposite MulOpposite.op mul	—	iUnion_image_right
iUnion_op_vadd_set 📖	mathematical	—	iUnion Set instMembership HVAdd.hVAdd AddOpposite instHVAdd vaddSet Add.toVAddAddOpposite AddOpposite.op add	—	iUnion_image_right
iUnion_smul_eq_setOf_exists 📖	mathematical	—	iUnion Set smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction setOf instMembership	—	—
iUnion_vadd_eq_setOf_exists 📖	mathematical	—	iUnion HVAdd.hVAdd Set instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction setOf instMembership	—	iUnion_setOf iUnion_neg_vadd preimage_vadd
image_op_smul 📖	mathematical	—	Set MulOpposite smul Mul.toSMulMulOpposite image MulOpposite.op mul	—	image2_smul image2_mul image2_image_left image2_swap
image_op_smul_distrib 📖	mathematical	—	image DFunLike.coe MulOpposite Set smulSet Mul.toSMulMulOpposite MulOpposite.op	—	image_comm map_mul
image_op_vadd 📖	mathematical	—	HVAdd.hVAdd Set AddOpposite instHVAdd vadd Add.toVAddAddOpposite image AddOpposite.op add	—	image2_vadd image2_add image2_image_left image2_swap
image_op_vadd_distrib 📖	mathematical	—	image DFunLike.coe HVAdd.hVAdd AddOpposite Set instHVAdd vaddSet Add.toVAddAddOpposite AddOpposite.op	—	image_comm map_add
image_smul_distrib 📖	mathematical	—	image DFunLike.coe Set smulSet	—	image_comm map_mul
image_vadd_distrib 📖	mathematical	—	image DFunLike.coe HVAdd.hVAdd Set instHVAdd vaddSet Add.toVAdd	—	image_comm map_add
inv_op_smul_set_distrib 📖	mathematical	—	Set inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid MulOpposite smulSet 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_set_distrib 📖	mathematical	—	Set inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid smulSet 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
isCentralScalar 📖	mathematical	—	IsCentralScalar Set smulSet MulOpposite	—	IsCentralScalar.op_smul_eq_smul
isCentralVAdd 📖	mathematical	—	IsCentralVAdd Set vaddSet AddOpposite	—	IsCentralVAdd.op_vadd_eq_vadd
isScalarTower 📖	mathematical	—	IsScalarTower Set smulSet	—	image_congr smul_assoc image_image
isScalarTower' 📖	mathematical	—	IsScalarTower Set smulSet smul	—	image2_image_left_comm smul_assoc
isScalarTower'' 📖	mathematical	—	IsScalarTower Set smul	—	image2_assoc smul_assoc
mem_invOf_smul_set 📖	mathematical	—	Set instMembership smulSet SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Invertible.invOf MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass MulOne.toOne	—	mem_inv_smul_set_iff
mem_inv_smul_set_iff 📖	mathematical	—	Set instMembership smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
mem_neg_vadd_set_iff 📖	mathematical	—	Set instMembership HVAdd.hVAdd instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	mem_image neg_vadd_eq_iff
mem_smul_set_iff_inv_smul_mem 📖	mathematical	—	Set instMembership smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	mem_image_equiv
mem_smul_set_inv 📖	mathematical	—	Set instMembership smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	mul_inv_rev inv_inv
mem_vadd_set_iff_neg_vadd_mem 📖	mathematical	—	Set instMembership HVAdd.hVAdd instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	mem_image_equiv
mem_vadd_set_neg 📖	mathematical	—	Set instMembership HVAdd.hVAdd instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	mem_vadd_set_iff_neg_vadd_mem mem_neg neg_add_rev neg_neg
mul_pair 📖	mathematical	—	Set mul instInsert instSingletonSet instUnion MulOpposite smulSet Mul.toSMulMulOpposite MulOpposite.op	—	insert_eq mul_union mul_singleton
mul_subset_iff_left 📖	mathematical	—	Set instHasSubset mul smulSet	—	image2_subset_iff_left
mul_subset_iff_right 📖	mathematical	—	Set instHasSubset mul MulOpposite smulSet Mul.toSMulMulOpposite MulOpposite.op	—	image2_subset_iff_right
neg_op_vadd_set_distrib 📖	mathematical	—	Set neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid HVAdd.hVAdd AddOpposite instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddOpposite.instAddMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toOppositeAddAction AddOpposite.op AddMonoid.toAddAction	—	ext mem_neg mem_vadd_set_iff_neg_vadd_mem neg_neg neg_add_rev
neg_vadd_set_distrib 📖	mathematical	—	Set neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid HVAdd.hVAdd instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction AddOpposite AddOpposite.instAddMonoid AddMonoid.toOppositeAddAction AddOpposite.op	—	ext mem_neg mem_vadd_set_iff_neg_vadd_mem neg_neg neg_add_rev
op_smul_inter_ne_empty_iff 📖	mathematical	—	Set instMembership MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid MulOpposite.unop	—	nonempty_iff_ne_empty op_smul_inter_nonempty_iff
op_smul_inter_nonempty_iff 📖	mathematical	—	Nonempty Set instInter MulOpposite smulSet SemigroupAction.toSMul Monoid.toSemigroup MulOpposite.instMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toOppositeMulAction instMembership MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid MulOpposite.unop	—	mem_smul_set inv_mul_cancel_left mem_inter mul_inv_cancel_left
op_smul_set_mul_eq_mul_smul_set 📖	mathematical	—	Set mul Semigroup.toMul MulOpposite smulSet Mul.toSMulMulOpposite MulOpposite.op	—	op_smul_set_smul_eq_smul_smul_set mul_assoc
op_smul_set_subset_mul 📖	mathematical	Set instMembership	instHasSubset MulOpposite smulSet Mul.toSMulMulOpposite MulOpposite.op mul	—	image_subset_image2_left
op_vadd_inter_ne_empty_iff 📖	mathematical	—	Set instMembership AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid AddOpposite.unop	—	nonempty_iff_ne_empty op_vadd_inter_nonempty_iff
op_vadd_inter_nonempty_iff 📖	mathematical	—	Nonempty Set instInter HVAdd.hVAdd AddOpposite instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddOpposite.instAddMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toOppositeAddAction instMembership AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid AddOpposite.unop	—	mem_vadd_set neg_add_cancel_left mem_inter add_neg_cancel_left
op_vadd_set_add_eq_add_vadd_set 📖	mathematical	—	Set add AddSemigroup.toAdd HVAdd.hVAdd AddOpposite instHVAdd vaddSet Add.toVAddAddOpposite AddOpposite.op Add.toVAdd	—	op_vadd_set_vadd_eq_vadd_vadd_set add_assoc
op_vadd_set_subset_add 📖	mathematical	Set instMembership	instHasSubset HVAdd.hVAdd AddOpposite instHVAdd vaddSet Add.toVAddAddOpposite AddOpposite.op add	—	image_subset_image2_left
pair_add 📖	mathematical	—	Set add instInsert instSingletonSet instUnion HVAdd.hVAdd instHVAdd vaddSet Add.toVAdd	—	insert_eq union_add singleton_add
pair_mul 📖	mathematical	—	Set mul instInsert instSingletonSet instUnion smulSet	—	insert_eq union_mul singleton_mul
pairwiseDisjoint_smul_iff 📖	mathematical	—	PairwiseDisjoint Set CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice smulSet InjOn SProd.sprod instSProd	—	pairwiseDisjoint_image_right_iff mul_right_injective
pairwiseDisjoint_vadd_iff 📖	mathematical	—	PairwiseDisjoint Set CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice HVAdd.hVAdd instHVAdd vaddSet Add.toVAdd InjOn SProd.sprod instSProd	—	pairwiseDisjoint_image_right_iff add_right_injective
pairwise_disjoint_smul_iff 📖	mathematical	—	Pairwise Function.onFun Set Disjoint CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	not_imp_not inv_one one_mul
pairwise_disjoint_vadd_iff 📖	mathematical	—	Pairwise Function.onFun Set Disjoint CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice HVAdd.hVAdd instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	disjoint_vadd_set_right AddSemigroupAction.add_vadd not_imp_not not_ne_iff not_disjoint_iff_nonempty_inter neg_zero zero_add neg_add_eq_zero
preimage_smul 📖	mathematical	—	preimage SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Set smulSet InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Equiv.image_symm_eq_preimage
preimage_smul_inv 📖	mathematical	—	preimage SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Set smulSet	—	preimage_smul
preimage_vadd 📖	mathematical	—	preimage HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction Set vaddSet NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	Equiv.image_symm_eq_preimage
preimage_vadd_neg 📖	mathematical	—	preimage HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Set vaddSet	—	preimage_vadd
range_add 📖	mathematical	—	range HVAdd.hVAdd Set instHVAdd vaddSet Add.toVAdd	—	range_vadd
range_mul 📖	mathematical	—	range Set smulSet	—	range_smul
smulCommClass 📖	mathematical	—	SMulCommClass Set smul	—	image2_left_comm SMulCommClass.smul_comm
smulCommClass_set 📖	mathematical	—	SMulCommClass Set smulSet	—	Function.Commute.set_image SMulCommClass.smul_comm
smulCommClass_set' 📖	mathematical	—	SMulCommClass Set smulSet smul	—	image_image2_distrib_right SMulCommClass.smul_comm
smulCommClass_set'' 📖	mathematical	—	SMulCommClass Set smul smulSet	—	SMulCommClass.symm smulCommClass_set'
smul_div_smul_comm 📖	mathematical	—	Set div DivInvMonoid.toDiv Group.toDivInvMonoid CommGroup.toGroup smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid MulAction.toSemigroupAction Monoid.toMulAction	—	image_congr mul_div_mul_comm singleton_div_singleton
smul_graphOn 📖	mathematical	—	Set smulSet SemigroupAction.toSMul Monoid.toSemigroup Prod.instMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MulAction.toSemigroupAction Monoid.toMulAction graphOn DFunLike.coe MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toDiv	—	ext map_mul MonoidHomClass.toMulHomClass map_inv mul_left_comm mul_comm
smul_graphOn_univ 📖	mathematical	—	Set smulSet SemigroupAction.toSMul Monoid.toSemigroup Prod.instMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MulAction.toSemigroupAction Monoid.toMulAction graphOn DFunLike.coe univ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toDiv	—	smul_graphOn smul_set_univ
smul_inter_ne_empty_iff 📖	mathematical	—	Set instMembership MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	nonempty_iff_ne_empty smul_inter_nonempty_iff
smul_inter_ne_empty_iff' 📖	mathematical	—	Set instMembership DivInvMonoid.toDiv Group.toDivInvMonoid	—	nonempty_iff_ne_empty smul_inter_nonempty_iff'
smul_inter_nonempty_iff 📖	mathematical	—	Nonempty Set instInter smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction instMembership MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	mem_smul_set mul_inv_cancel_right mem_inter inv_mul_cancel_right
smul_inter_nonempty_iff' 📖	mathematical	—	Nonempty Set instInter smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction instMembership DivInvMonoid.toDiv	—	div_eq_mul_inv
smul_mem_smul_set_iff 📖	mathematical	—	Set instMembership smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	Function.Injective.mem_set_image MulAction.injective
smul_set_compl 📖	mathematical	—	Set smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Compl.compl instCompl	—	compl_eq_univ_diff smul_set_sdiff smul_set_univ
smul_set_eq_univ 📖	mathematical	—	Set smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction univ	—	smul_eq_iff_eq_inv_smul smul_set_univ
smul_set_iInter 📖	mathematical	—	Set smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction iInter	—	image_iInter MulAction.bijective
smul_set_inter 📖	mathematical	—	Set smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instInter	—	image_inter MulAction.injective
smul_set_pi 📖	mathematical	—	Set smulSet Pi.instSMul SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction pi	—	smul_set_pi_of_surjective Function.Bijective.surjective MulAction.bijective
smul_set_pi_of_isUnit 📖	mathematical	IsUnit	Set smulSet Pi.instSMul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pi	—	CanLift.prf instCanLiftUnitsValIsUnit smul_set_pi
smul_set_prod 📖	mathematical	—	Set smulSet Prod.instSMul SProd.sprod instSProd	—	prodMap_image_prod
smul_set_sdiff 📖	mathematical	—	Set smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instSDiff	—	image_diff MulAction.injective
smul_set_subset_iff_subset_inv_smul_set 📖	mathematical	—	Set instHasSubset smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	image_subset_iff Equiv.image_symm_eq_preimage
smul_set_subset_mul 📖	mathematical	Set instMembership	instHasSubset smulSet mul	—	image_subset_image2_right
smul_set_subset_smul_set_iff 📖	mathematical	—	Set instHasSubset smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	image_subset_image_iff MulAction.injective
smul_set_symmDiff 📖	mathematical	—	Set smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra instSDiff	—	image_symmDiff MulAction.injective
smul_set_univ 📖	mathematical	—	Set smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction univ	—	image_univ_of_surjective MulAction.surjective
smul_univ 📖	mathematical	Nonempty	Set smul SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction univ	—	eq_univ_of_forall smul_inv_smul
subset_smul_set_iff 📖	mathematical	—	Set instHasSubset smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	image_subset_iff Equiv.image_eq_preimage_symm
subset_vadd_set_iff 📖	mathematical	—	Set instHasSubset HVAdd.hVAdd instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	image_subset_iff Equiv.image_eq_preimage_symm
vaddAssocClass 📖	mathematical	—	VAddAssocClass Set vaddSet	—	image_congr vadd_assoc image_image
vaddAssocClass' 📖	mathematical	—	VAddAssocClass Set vaddSet vadd	—	image2_image_left_comm vadd_assoc
vaddAssocClass'' 📖	mathematical	—	VAddAssocClass Set vadd	—	image2_assoc vadd_assoc
vaddCommClass 📖	mathematical	—	VAddCommClass Set vadd	—	image2_left_comm VAddCommClass.vadd_comm
vaddCommClass_set 📖	mathematical	—	VAddCommClass Set vaddSet	—	Function.Commute.set_image VAddCommClass.vadd_comm
vaddCommClass_set' 📖	mathematical	—	VAddCommClass Set vaddSet vadd	—	image_image2_distrib_right VAddCommClass.vadd_comm
vaddCommClass_set'' 📖	mathematical	—	VAddCommClass Set vadd vaddSet	—	VAddCommClass.symm vaddCommClass_set'
vadd_graphOn 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup Prod.instAddMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddMonoid.toAddAction graphOn DFunLike.coe AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toSub	—	ext mem_vadd_set_iff_neg_vadd_mem mem_graphOn map_add AddMonoidHomClass.toAddHomClass map_neg eq_neg_add_iff_add_eq add_left_comm neg_add_eq_iff_eq_add add_sub_right_comm sub_eq_iff_eq_add add_comm
vadd_graphOn_univ 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup Prod.instAddMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddAction.toAddSemigroupAction AddMonoid.toAddAction graphOn DFunLike.coe univ AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toSub	—	vadd_graphOn vadd_set_univ
vadd_inter_ne_empty_iff 📖	mathematical	—	Set instMembership AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	nonempty_iff_ne_empty vadd_inter_nonempty_iff
vadd_inter_ne_empty_iff' 📖	mathematical	—	Set instMembership SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	nonempty_iff_ne_empty vadd_inter_nonempty_iff'
vadd_inter_nonempty_iff 📖	mathematical	—	Nonempty Set instInter HVAdd.hVAdd instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction instMembership AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	mem_vadd_set add_neg_cancel_right mem_inter neg_add_cancel_right
vadd_inter_nonempty_iff' 📖	mathematical	—	Nonempty Set instInter HVAdd.hVAdd instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction instMembership SubNegMonoid.toSub	—	vadd_inter_nonempty_iff sub_eq_add_neg
vadd_mem_vadd_set_iff 📖	mathematical	—	Set instMembership HVAdd.hVAdd instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	—	Function.Injective.mem_set_image AddAction.injective
vadd_set_compl 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction Compl.compl instCompl	—	compl_eq_univ_diff vadd_set_sdiff vadd_set_univ
vadd_set_eq_univ 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction univ	—	vadd_eq_iff_eq_neg_vadd vadd_set_univ
vadd_set_iInter 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction iInter	—	image_iInter AddAction.bijective
vadd_set_inter 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction instInter	—	image_inter AddAction.injective
vadd_set_pi 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd vaddSet Pi.instVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction pi	—	vadd_set_pi_of_surjective Function.Bijective.surjective AddAction.bijective
vadd_set_pi_of_isAddUnit 📖	mathematical	IsAddUnit	HVAdd.hVAdd Set instHVAdd vaddSet Pi.instVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction pi	—	CanLift.prf instCanLiftAddUnitsValIsAddUnit vadd_set_pi
vadd_set_prod 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd vaddSet Prod.instVAdd SProd.sprod instSProd	—	prodMap_image_prod
vadd_set_sdiff 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction instSDiff	—	image_diff AddAction.injective
vadd_set_subset_add 📖	mathematical	Set instMembership	instHasSubset HVAdd.hVAdd instHVAdd vaddSet Add.toVAdd add	—	image_subset_image2_right
vadd_set_subset_iff_subset_neg_vadd_set 📖	mathematical	—	Set instHasSubset HVAdd.hVAdd instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	image_subset_iff Equiv.image_symm_eq_preimage
vadd_set_subset_vadd_set_iff 📖	mathematical	—	Set instHasSubset HVAdd.hVAdd instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	—	image_subset_image_iff AddAction.injective
vadd_set_symmDiff 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra instSDiff	—	image_symmDiff AddAction.injective
vadd_set_univ 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction univ	—	image_univ_of_surjective AddAction.surjective
vadd_sub_vadd_comm 📖	mathematical	—	Set sub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup HVAdd.hVAdd instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction	—	image_congr singleton_add add_sub_add_comm singleton_sub_singleton
vadd_univ 📖	mathematical	Nonempty	HVAdd.hVAdd Set instHVAdd vadd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction univ	—	eq_univ_of_forall vadd_neg_vadd

---

← Back to Index