Stabilizer

📁 Source: Mathlib/Algebra/Pointwise/Stabilizer.lean

Statistics

Metric	Count
Definitions	0
Theorems add_stabilizer_self, map_stabilizer_le, mem_stabilizer_finset, mem_stabilizer_finset', mem_stabilizer_finset_iff_subset_vadd_finset, mem_stabilizer_finset_iff_vadd_finset_subset, mem_stabilizer_set, mem_stabilizer_set', mem_stabilizer_set_iff_subset_vadd_set, mem_stabilizer_set_iff_vadd_set_subset, op_vadd_set_stabilizer_subset, stabilizer_addSubgroup, stabilizer_addSubgroup_op, stabilizer_add_self, stabilizer_coe_finset, stabilizer_empty, stabilizer_finite, stabilizer_finset_empty, stabilizer_finset_singleton, stabilizer_finset_univ, stabilizer_image_coe_quotient, stabilizer_inf_stabilizer_le_stabilizer_apply₂, stabilizer_inf_stabilizer_le_stabilizer_inter, stabilizer_inf_stabilizer_le_stabilizer_sdiff, stabilizer_inf_stabilizer_le_stabilizer_union, stabilizer_op_addSubgroup, stabilizer_singleton, stabilizer_subset_sub_right, stabilizer_union_eq_left, stabilizer_union_eq_right, stabilizer_univ, vadd_set_stabilizer_subset, map_stabilizer_le, mem_stabilizer_finset, mem_stabilizer_finset', mem_stabilizer_finset_iff_smul_finset_subset, mem_stabilizer_finset_iff_subset_smul_finset, mem_stabilizer_set, mem_stabilizer_set', mem_stabilizer_set_iff_smul_set_subset, mem_stabilizer_set_iff_subset_smul_set, mul_stabilizer_self, op_smul_set_stabilizer_subset, smul_set_stabilizer_subset, stabilizer_coe_finset, stabilizer_empty, stabilizer_finite, stabilizer_finset_empty, stabilizer_finset_singleton, stabilizer_finset_univ, stabilizer_image_coe_quotient, stabilizer_inf_stabilizer_le_stabilizer_apply₂, stabilizer_inf_stabilizer_le_stabilizer_inter, stabilizer_inf_stabilizer_le_stabilizer_sdiff, stabilizer_inf_stabilizer_le_stabilizer_union, stabilizer_mul_self, stabilizer_op_subgroup, stabilizer_singleton, stabilizer_subgroup, stabilizer_subgroup_op, stabilizer_subset_div_right, stabilizer_union_eq_left, stabilizer_union_eq_right, stabilizer_univ	64
Total	64

AddAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_stabilizer_self 📖	mathematical	—	Set Set.add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SetLike.coe AddSubgroup AddSubgroup.instSetLike stabilizer Set.addActionSet AddMonoid.toAddAction	—	add_comm stabilizer_add_self
map_stabilizer_le 📖	mathematical	—	AddSubgroup Preorder.toLE PartialOrder.toPreorder AddSubgroup.instPartialOrder AddSubgroup.map stabilizer Set Set.addActionSet SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddMonoid.toAddAction Set.image DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike	—	AddSubgroup.mem_map mem_stabilizer_iff Set.image_vadd_distrib AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass
mem_stabilizer_finset 📖	mathematical	—	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike stabilizer Finset Finset.addActionFinset SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Finset.instMembership HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction	—	stabilizer_coe_finset mem_stabilizer_set Finset.mem_coe
mem_stabilizer_finset' 📖	mathematical	—	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike stabilizer Finset Finset.addActionFinset SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Finset.instMembership HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction	—	AddSubgroup.neg_mem_iff mem_stabilizer_finset_iff_subset_vadd_finset Finset.mem_neg_vadd_finset_iff Finset.subset_iff
mem_stabilizer_finset_iff_subset_vadd_finset 📖	mathematical	—	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike stabilizer Finset Finset.addActionFinset SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Finset.instHasSubset HVAdd.hVAdd instHVAdd Finset.vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction	—	mem_stabilizer_iff Finset.subset_iff_eq_of_card_le Eq.le Finset.card_vadd_finset
mem_stabilizer_finset_iff_vadd_finset_subset 📖	mathematical	—	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike stabilizer Finset Finset.addActionFinset SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Finset.instHasSubset HVAdd.hVAdd instHVAdd Finset.vaddFinset AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction	—	mem_stabilizer_iff Finset.subset_iff_eq_of_card_le Eq.ge Finset.card_vadd_finset
mem_stabilizer_set 📖	mathematical	—	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike stabilizer Set Set.addActionSet SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Set.instMembership HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction	—	mem_stabilizer_iff Set.vadd_mem_vadd_set_iff Set.ext_iff Set.mem_vadd_set_iff_neg_vadd_mem Equiv.forall_congr' vadd_neg_vadd
mem_stabilizer_set' 📖	mathematical	—	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike stabilizer Set Set.addActionSet SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Set.instMembership HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction	—	CanLift.prf Set.instCanLiftFinsetCoeFinite stabilizer_coe_finset mem_stabilizer_finset' SetLike.mem_coe
mem_stabilizer_set_iff_subset_vadd_set 📖	mathematical	—	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike stabilizer Set Set.addActionSet SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Set.instHasSubset HVAdd.hVAdd instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction	—	CanLift.prf Set.instCanLiftFinsetCoeFinite stabilizer_coe_finset mem_stabilizer_finset_iff_subset_vadd_finset Finset.coe_vadd_finset Finset.coe_subset
mem_stabilizer_set_iff_vadd_set_subset 📖	mathematical	—	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike stabilizer Set Set.addActionSet SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Set.instHasSubset HVAdd.hVAdd instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction	—	CanLift.prf Set.instCanLiftFinsetCoeFinite stabilizer_coe_finset mem_stabilizer_finset_iff_vadd_finset_subset Finset.coe_vadd_finset Finset.coe_subset
op_vadd_set_stabilizer_subset 📖	mathematical	Set Set.instMembership	Set.instHasSubset HVAdd.hVAdd AddOpposite instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddOpposite.instAddMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddSemigroupAction AddMonoid.toOppositeAddAction AddOpposite.op SetLike.coe AddSubgroup AddSubgroup.instSetLike stabilizer Set.addActionSet AddMonoid.toAddAction	—	Set.vadd_set_subset_iff Set.vadd_mem_vadd_set
stabilizer_addSubgroup 📖	mathematical	—	stabilizer Set Set.addActionSet SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddMonoid.toAddAction SetLike.coe AddSubgroup AddSubgroup.instSetLike	—	SetLike.ext_iff mem_stabilizer_set add_zero SetLike.mem_coe AddSubgroup.zero_mem AddSubgroup.add_mem_cancel_left
stabilizer_addSubgroup_op 📖	mathematical	—	stabilizer Set AddOpposite Set.addActionSet SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddOpposite.instAddAction AddMonoid.toAddAction SetLike.coe AddSubgroup AddOpposite.instAddGroup AddSubgroup.instSetLike AddSubgroup.unop	—	SetLike.ext_iff mem_stabilizer_set AddSubgroup.zero_mem zero_add AddSubgroup.add_mem_cancel_right
stabilizer_add_self 📖	mathematical	—	Set Set.add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SetLike.coe AddSubgroup AddSubgroup.instSetLike stabilizer Set.addActionSet AddMonoid.toAddAction	—	Set.ext mem_stabilizer_iff Set.vadd_mem_vadd_set AddSubgroup.zero_mem zero_add
stabilizer_coe_finset 📖	mathematical	—	stabilizer Set Set.addActionSet SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SetLike.coe Finset Finset.instSetLike Finset.addActionFinset	—	AddSubgroup.ext mem_stabilizer_iff Finset.coe_vadd_finset
stabilizer_empty 📖	mathematical	—	stabilizer Set Set.addActionSet SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Set.instEmptyCollection Top.top AddSubgroup AddSubgroup.instTop	—	AddSubgroup.coe_eq_univ Set.eq_univ_of_forall Set.vadd_set_empty
stabilizer_finite 📖	mathematical	Set.Nonempty	Set.Finite SetLike.coe AddSubgroup AddSubgroup.instSetLike stabilizer Set Set.addActionSet SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddMonoid.toAddAction	—	Set.Finite.subset Set.Finite.sub Set.finite_singleton stabilizer_subset_sub_right
stabilizer_finset_empty 📖	mathematical	—	stabilizer Finset Finset.addActionFinset SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Finset.instEmptyCollection Top.top AddSubgroup AddSubgroup.instTop	—	AddSubgroup.coe_eq_univ Set.eq_univ_of_forall Finset.vadd_finset_empty
stabilizer_finset_singleton 📖	mathematical	—	stabilizer Finset Finset.addActionFinset SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Finset.instSingleton	—	AddSubgroup.ext mem_stabilizer_iff Finset.vadd_finset_singleton
stabilizer_finset_univ 📖	mathematical	—	stabilizer Finset Finset.addActionFinset SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Finset.univ Top.top AddSubgroup AddSubgroup.instTop	—	AddSubgroup.ext mem_stabilizer_iff Finset.vadd_finset_univ AddSubgroup.mem_top
stabilizer_image_coe_quotient 📖	mathematical	—	stabilizer HasQuotient.Quotient AddSubgroup AddCommGroup.toAddGroup QuotientAddGroup.instHasQuotientAddSubgroup Set Set.addActionSet SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddMonoid.toAddAction QuotientAddGroup.Quotient.addGroup AddSubgroup.normal_of_comm Set.image Bot.bot AddSubgroup.instBot	—	AddSubgroup.ext AddSubgroup.normal_of_comm QuotientAddGroup.induction_on mem_stabilizer_iff AddSubgroup.mem_bot QuotientAddGroup.eq_zero_iff Set.image_vadd_distrib AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass stabilizer_add_self add_vadd_comm Set.vaddCommClass_set' vaddCommClass_self
stabilizer_inf_stabilizer_le_stabilizer_apply₂ 📖	mathematical	HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddSemigroupAction	AddSubgroup Preorder.toLE PartialOrder.toPreorder AddSubgroup.instPartialOrder AddSubgroup.instMin stabilizer Set.addActionSet	—	SetLike.le_def instIsConcreteLE AddSubgroup.mem_inf mem_stabilizer_iff
stabilizer_inf_stabilizer_le_stabilizer_inter 📖	mathematical	—	AddSubgroup Preorder.toLE PartialOrder.toPreorder AddSubgroup.instPartialOrder AddSubgroup.instMin stabilizer Set Set.addActionSet SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Set.instInter	—	stabilizer_inf_stabilizer_le_stabilizer_apply₂ Set.vadd_set_inter
stabilizer_inf_stabilizer_le_stabilizer_sdiff 📖	mathematical	—	AddSubgroup Preorder.toLE PartialOrder.toPreorder AddSubgroup.instPartialOrder AddSubgroup.instMin stabilizer Set Set.addActionSet SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Set.instSDiff	—	stabilizer_inf_stabilizer_le_stabilizer_apply₂ Set.vadd_set_sdiff
stabilizer_inf_stabilizer_le_stabilizer_union 📖	mathematical	—	AddSubgroup Preorder.toLE PartialOrder.toPreorder AddSubgroup.instPartialOrder AddSubgroup.instMin stabilizer Set Set.addActionSet SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Set.instUnion	—	stabilizer_inf_stabilizer_le_stabilizer_apply₂ Set.vadd_set_union
stabilizer_op_addSubgroup 📖	mathematical	—	stabilizer AddOpposite Set AddOpposite.instAddGroup Set.addActionSet SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddMonoid.toOppositeAddAction SetLike.coe AddSubgroup AddSubgroup.instSetLike AddSubgroup.op	—	SetLike.ext_iff mem_stabilizer_set SetLike.mem_coe AddSubgroup.mem_op AddOpposite.forall zero_add AddSubgroup.zero_mem AddSubgroup.add_mem_cancel_right
stabilizer_singleton 📖	mathematical	—	stabilizer Set Set.addActionSet SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Set.instSingletonSet	—	AddSubgroup.ext mem_stabilizer_iff Set.vadd_set_singleton Set.singleton_eq_singleton_iff
stabilizer_subset_sub_right 📖	mathematical	Set Set.instMembership	Set.instHasSubset SetLike.coe AddSubgroup AddSubgroup.instSetLike stabilizer Set.addActionSet SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddMonoid.toAddAction Set.sub SubNegMonoid.toSub Set.instSingletonSet	—	vadd_eq_add mem_stabilizer_set Set.mem_singleton add_sub_cancel_right
stabilizer_union_eq_left 📖	—	Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice AddSubgroup Preorder.toLE PartialOrder.toPreorder AddSubgroup.instPartialOrder stabilizer Set.addActionSet SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Set.instUnion	—	—	le_antisymm le_inf_iff le_refl stabilizer_inf_stabilizer_le_stabilizer_sdiff Set.union_diff_cancel_right Set.subset_empty_iff Set.disjoint_iff_inter_eq_empty stabilizer_inf_stabilizer_le_stabilizer_union
stabilizer_union_eq_right 📖	—	Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice AddSubgroup Preorder.toLE PartialOrder.toPreorder AddSubgroup.instPartialOrder stabilizer Set.addActionSet SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Set.instUnion	—	—	Set.union_comm stabilizer_union_eq_left Disjoint.symm
stabilizer_univ 📖	mathematical	—	stabilizer Set Set.addActionSet SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Set.univ Top.top AddSubgroup AddSubgroup.instTop	—	AddSubgroup.ext mem_stabilizer_iff Set.vadd_set_univ AddSubgroup.mem_top
vadd_set_stabilizer_subset 📖	mathematical	Set Set.instMembership	Set.instHasSubset HVAdd.hVAdd instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup toAddSemigroupAction AddMonoid.toAddAction SetLike.coe AddSubgroup AddSubgroup.instSetLike stabilizer Set.addActionSet	—	IsCentralVAdd.op_vadd_eq_vadd Set.isCentralVAdd AddCommSemigroup.isCentralVAdd op_vadd_set_stabilizer_subset

MulAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_stabilizer_le 📖	mathematical	—	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder Subgroup.map stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid Monoid.toMulAction Set.image DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	—	Set.image_smul_distrib MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass
mem_stabilizer_finset 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike stabilizer Finset Finset.mulActionFinset DivInvMonoid.toMonoid Group.toDivInvMonoid Finset.instMembership SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction	—	—
mem_stabilizer_finset' 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike stabilizer Finset Finset.mulActionFinset DivInvMonoid.toMonoid Group.toDivInvMonoid Finset.instMembership SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction	—	Subgroup.inv_mem_iff mem_stabilizer_finset_iff_subset_smul_finset
mem_stabilizer_finset_iff_smul_finset_subset 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike stabilizer Finset Finset.mulActionFinset DivInvMonoid.toMonoid Group.toDivInvMonoid Finset.instHasSubset Finset.smulFinset SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction	—	mem_stabilizer_iff Finset.subset_iff_eq_of_card_le Eq.ge Finset.card_smul_finset
mem_stabilizer_finset_iff_subset_smul_finset 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike stabilizer Finset Finset.mulActionFinset DivInvMonoid.toMonoid Group.toDivInvMonoid Finset.instHasSubset Finset.smulFinset SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction	—	mem_stabilizer_iff Finset.subset_iff_eq_of_card_le Eq.le Finset.card_smul_finset
mem_stabilizer_set 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid Set.instMembership SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction	—	mem_stabilizer_iff Set.smul_mem_smul_set_iff Equiv.forall_congr' smul_inv_smul
mem_stabilizer_set' 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid Set.instMembership SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction	—	CanLift.prf Set.instCanLiftFinsetCoeFinite stabilizer_coe_finset
mem_stabilizer_set_iff_smul_set_subset 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid Set.instHasSubset Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction	—	CanLift.prf Set.instCanLiftFinsetCoeFinite stabilizer_coe_finset mem_stabilizer_finset_iff_smul_finset_subset Finset.coe_smul_finset Finset.coe_subset
mem_stabilizer_set_iff_subset_smul_set 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid Set.instHasSubset Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction	—	CanLift.prf Set.instCanLiftFinsetCoeFinite stabilizer_coe_finset mem_stabilizer_finset_iff_subset_smul_finset Finset.coe_smul_finset Finset.coe_subset
mul_stabilizer_self 📖	mathematical	—	Set Set.mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup SetLike.coe Subgroup Subgroup.instSetLike stabilizer Set.mulActionSet Monoid.toMulAction	—	mul_comm stabilizer_mul_self
op_smul_set_stabilizer_subset 📖	mathematical	Set Set.instMembership	Set.instHasSubset MulOpposite Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup MulOpposite.instMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid toSemigroupAction Monoid.toOppositeMulAction MulOpposite.op SetLike.coe Subgroup Subgroup.instSetLike stabilizer Set.mulActionSet Monoid.toMulAction	—	Set.smul_set_subset_iff Set.smul_mem_smul_set
smul_set_stabilizer_subset 📖	mathematical	Set Set.instMembership	Set.instHasSubset Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup toSemigroupAction Monoid.toMulAction SetLike.coe Subgroup Subgroup.instSetLike stabilizer Set.mulActionSet	—	IsCentralScalar.op_smul_eq_smul Set.isCentralScalar CommSemigroup.isCentralScalar op_smul_set_stabilizer_subset
stabilizer_coe_finset 📖	mathematical	—	stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid SetLike.coe Finset Finset.instSetLike Finset.mulActionFinset	—	Subgroup.ext Finset.coe_smul_finset
stabilizer_empty 📖	mathematical	—	stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid Set.instEmptyCollection Top.top Subgroup Subgroup.instTop	—	Subgroup.coe_eq_univ Set.eq_univ_of_forall Set.smul_set_empty
stabilizer_finite 📖	mathematical	Set.Nonempty	Set.Finite SetLike.coe Subgroup Subgroup.instSetLike stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid Monoid.toMulAction	—	Set.Finite.subset Set.Finite.div Set.finite_singleton stabilizer_subset_div_right
stabilizer_finset_empty 📖	mathematical	—	stabilizer Finset Finset.mulActionFinset DivInvMonoid.toMonoid Group.toDivInvMonoid Finset.instEmptyCollection Top.top Subgroup Subgroup.instTop	—	Subgroup.coe_eq_univ Set.eq_univ_of_forall Finset.smul_finset_empty
stabilizer_finset_singleton 📖	mathematical	—	stabilizer Finset Finset.mulActionFinset DivInvMonoid.toMonoid Group.toDivInvMonoid Finset.instSingleton	—	Subgroup.ext Finset.smul_finset_singleton
stabilizer_finset_univ 📖	mathematical	—	stabilizer Finset Finset.mulActionFinset DivInvMonoid.toMonoid Group.toDivInvMonoid Finset.univ Top.top Subgroup Subgroup.instTop	—	Subgroup.ext Finset.smul_finset_univ
stabilizer_image_coe_quotient 📖	mathematical	—	stabilizer HasQuotient.Quotient Subgroup CommGroup.toGroup QuotientGroup.instHasQuotientSubgroup Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid Monoid.toMulAction QuotientGroup.Quotient.group Subgroup.normal_of_comm Set.image Bot.bot Subgroup.instBot	—	Subgroup.ext Subgroup.normal_of_comm QuotientGroup.induction_on Set.image_smul_distrib MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass stabilizer_mul_self mul_smul_comm Set.smulCommClass_set' smulCommClass_self
stabilizer_inf_stabilizer_le_stabilizer_apply₂ 📖	mathematical	Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toSemigroupAction	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder Subgroup.instMin stabilizer Set.mulActionSet	—	instIsConcreteLE
stabilizer_inf_stabilizer_le_stabilizer_inter 📖	mathematical	—	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder Subgroup.instMin stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid Set.instInter	—	stabilizer_inf_stabilizer_le_stabilizer_apply₂ Set.smul_set_inter
stabilizer_inf_stabilizer_le_stabilizer_sdiff 📖	mathematical	—	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder Subgroup.instMin stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid Set.instSDiff	—	stabilizer_inf_stabilizer_le_stabilizer_apply₂ Set.smul_set_sdiff
stabilizer_inf_stabilizer_le_stabilizer_union 📖	mathematical	—	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder Subgroup.instMin stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid Set.instUnion	—	stabilizer_inf_stabilizer_le_stabilizer_apply₂ Set.smul_set_union
stabilizer_mul_self 📖	mathematical	—	Set Set.mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SetLike.coe Subgroup Subgroup.instSetLike stabilizer Set.mulActionSet Monoid.toMulAction	—	Set.ext mem_stabilizer_iff Set.smul_mem_smul_set Subgroup.one_mem one_mul
stabilizer_op_subgroup 📖	mathematical	—	stabilizer MulOpposite Set MulOpposite.instGroup Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid Monoid.toOppositeMulAction SetLike.coe Subgroup Subgroup.instSetLike Subgroup.op	—	one_mul Subgroup.one_mem Subgroup.mul_mem_cancel_right
stabilizer_singleton 📖	mathematical	—	stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid Set.instSingletonSet	—	Subgroup.ext Set.smul_set_singleton
stabilizer_subgroup 📖	mathematical	—	stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid Monoid.toMulAction SetLike.coe Subgroup Subgroup.instSetLike	—	mul_one Subgroup.one_mem Subgroup.mul_mem_cancel_left
stabilizer_subgroup_op 📖	mathematical	—	stabilizer Set MulOpposite Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid MulOpposite.instMulAction Monoid.toMulAction SetLike.coe Subgroup MulOpposite.instGroup Subgroup.instSetLike Subgroup.unop	—	Subgroup.one_mem one_mul Subgroup.mul_mem_cancel_right
stabilizer_subset_div_right 📖	mathematical	Set Set.instMembership	Set.instHasSubset SetLike.coe Subgroup Subgroup.instSetLike stabilizer Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid Monoid.toMulAction Set.div DivInvMonoid.toDiv Set.instSingletonSet	—	smul_eq_mul mem_stabilizer_set Set.mem_singleton mul_div_cancel_right
stabilizer_union_eq_left 📖	—	Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder stabilizer Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid Set.instUnion	—	—	le_antisymm stabilizer_inf_stabilizer_le_stabilizer_sdiff Set.union_diff_cancel_right stabilizer_inf_stabilizer_le_stabilizer_union
stabilizer_union_eq_right 📖	—	Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder stabilizer Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid Set.instUnion	—	—	Set.union_comm stabilizer_union_eq_left Disjoint.symm
stabilizer_univ 📖	mathematical	—	stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid Set.univ Top.top Subgroup Subgroup.instTop	—	Subgroup.ext Set.smul_set_univ

---

← Back to Index