OfStabilizer

📁 Source: Mathlib/GroupTheory/GroupAction/SubMulAction/OfStabilizer.lean

Statistics

Metric	Count
Definitions ofStabilizer, ofStabilizer, conjMap, snoc, ofStabilizer, conjMap, snoc, ofStabilizer, instAddActionSubtypeMemAddSubgroupStabilizerSetElem, instMulActionSubtypeMemSubgroupStabilizerSetElem	10
Theorems stabilizerEquivStabilizer_compTriple, stabilizerEquivStabilizer_compTriple, smul_stabilizer_def, ENat_card_ofStabilizer_add_zero_eq, exists_vadd_of_last_eq, mem_ofStabilizer_iff, nat_card_ofStabilizer_add_zero_eq, nat_card_ofStabilizer_eq, neq_of_mem_ofStabilizer, notMem_val_image, conjMap_apply, conjMap_bijective, conjMap_comp, conjMap_comp_apply, conjMap_comp_neg_apply, neg_conjMap_comp_apply, snoc_castSucc, snoc_last, ofStabilizer_carrier, ENat_card_ofStabilizer_add_one_eq, exists_smul_of_last_eq, mem_ofStabilizer_iff, nat_card_ofStabilizer_add_one_eq, nat_card_ofStabilizer_eq, nat_card_ofStabilizer_eq_add_one, neq_of_mem_ofStabilizer, notMem_val_image, conjMap_apply, conjMap_bijective, conjMap_comp, conjMap_comp_apply, conjMap_comp_inv_apply, inv_conjMap_comp_apply, snoc_castSucc, snoc_last, ofStabilizer_carrier, stabilizer_compl, stabilizer_empty_eq_top, stabilizer_univ_eq_top	39
Total	49

AddAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
stabilizerEquivStabilizer_compTriple 📖	mathematical	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddSemigroupAction AddSemigroup.toAdd	CompTriple AddSubgroup SetLike.instMembership AddSubgroup.instSetLike stabilizer DFunLike.coe AddEquiv AddSubgroup.add EquivLike.toFunLike AddEquiv.instEquivLike stabilizerEquivStabilizer	—	neg_add_rev

MulAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
stabilizerEquivStabilizer_compTriple 📖	mathematical	SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toSemigroupAction MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	CompTriple Subgroup SetLike.instMembership Subgroup.instSetLike stabilizer DFunLike.coe MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike stabilizerEquivStabilizer	—	mul_inv_rev

SMul

Definitions

Name	Category	Theorems
ofStabilizer 📖	CompOp	6 math math: Equiv.Perm.stabilizer_isPreprimitive, MulAction.isPreprimitive_stabilizer_subgroup, alternatingGroup.stabilizer_isPreprimitive, MulAction.isPreprimitive_stabilizer_of_surjective, smul_stabilizer_def, alternatingGroup.stabilizer_subgroup_isPreprimitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul_stabilizer_def 📖	mathematical	—	Set Set.instMembership Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid Set.Elem ofStabilizer SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	—

SubAddAction

Definitions

Name	Category	Theorems
ofStabilizer 📖	CompOp	25 math math: notMem_val_image, ofStabilizer.conjMap_comp, ofFixingAddSubgroup_of_singleton_bijective, mem_ofStabilizer_iff, ofStabilizer.isMultiplyPretransitive_iff_of_conj, ofStabilizer.conjMap_comp_neg_apply, ofStabilizer.isPretransitive_iff, ofFixingAddSubgroup_insert_map_bijective, nat_card_ofStabilizer_eq, ofStabilizer.isMultiplyPretransitive_iff, ofStabilizer.conjMap_bijective, AddAction.isMultiplyPreprimitive_succ_iff_ofStabilizer, ofStabilizer.snoc_castSucc, ENat_card_ofStabilizer_add_zero_eq, fixingAddSubgroup_of_insert, ofStabilizer.neg_conjMap_comp_apply, nat_card_ofStabilizer_add_zero_eq, ofStabilizer_carrier, ofStabilizer.conjMap_comp_apply, ofStabilizer.isMultiplyPretransitive, AddAction.isPreprimitive_fixingAddSubgroup_insert_iff, AddAction.isMultiplyPreprimitive_ofStabilizer, mem_ofFixingAddSubgroup_insert_iff, ofStabilizer.isPretransitive_iff_of_conj, ofStabilizer.conjMap_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ENat_card_ofStabilizer_add_zero_eq 📖	mathematical	—	ENat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat ENat.card SubAddAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddAction.stabilizer AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.toAddSemigroupAction AddSubgroup.instAddAction instSetLike ofStabilizer AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Cardinal.mk_sum_compl map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass OrderRingHom.instRingHomClass add_comm Cardinal.mk_fintype Fintype.card_unique Nat.cast_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
exists_vadd_of_last_eq 📖	mathematical	—	HVAdd.hVAdd Function.Embedding instHVAdd Function.Embedding.vadd ofStabilizer.snoc	—	AddAction.exists_vadd_eq mem_ofStabilizer_iff vadd_left_cancel_iff EmbeddingLike.apply_eq_iff_eq Function.instEmbeddingLikeEmbedding Fin.castSucc_ne_last Function.Embedding.ext Fin.eq_castSucc_or_eq_last Fin.snoc_castSucc Function.Embedding.codRestrict_apply Fin.Embedding.snoc_last
mem_ofStabilizer_iff 📖	mathematical	—	SubAddAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddAction.stabilizer AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.toAddSemigroupAction AddSubgroup.instAddAction instSetLike ofStabilizer	—	—
nat_card_ofStabilizer_add_zero_eq 📖	mathematical	—	Nat.card SubAddAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddAction.stabilizer AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.toAddSemigroupAction AddSubgroup.instAddAction instSetLike ofStabilizer	—	Nat.subtype_card Finset.mem_compl Finset.mem_singleton mem_ofStabilizer_iff Finset.card_singleton Finset.card_compl_add_card Nat.card_eq_fintype_card
nat_card_ofStabilizer_eq 📖	mathematical	—	Nat.card SubAddAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddAction.stabilizer AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.toAddSemigroupAction AddSubgroup.instAddAction instSetLike ofStabilizer	—	nat_card_ofStabilizer_add_zero_eq
neq_of_mem_ofStabilizer 📖	—	—	—	—	Subtype.prop
notMem_val_image 📖	mathematical	—	Set Set.instMembership Set.image SubAddAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddAction.stabilizer AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.toAddSemigroupAction AddSubgroup.instAddAction instSetLike ofStabilizer	—	Subtype.prop Set.mem_singleton_iff
ofStabilizer_carrier 📖	mathematical	—	carrier AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddAction.stabilizer AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.toAddSemigroupAction AddSubgroup.instAddAction ofStabilizer Compl.compl Set Set.instCompl Set.instSingletonSet	—	—

SubAddAction.ofStabilizer

Definitions

Name	Category	Theorems
conjMap 📖	CompOp	6 math math: conjMap_comp, conjMap_comp_neg_apply, conjMap_bijective, neg_conjMap_comp_apply, conjMap_comp_apply, conjMap_apply
snoc 📖	CompOp	3 math math: snoc_last, snoc_castSucc, SubAddAction.exists_vadd_of_last_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conjMap_apply 📖	mathematical	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	SubAddAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddAction.stabilizer AddSubgroup.toAddGroup AddSubgroup.instAddAction SubAddAction.instSetLike SubAddAction.ofStabilizer DFunLike.coe AddActionHom AddEquiv AddSubgroup.add EquivLike.toFunLike AddEquiv.instEquivLike AddAction.stabilizerEquivStabilizer SubAddAction.vadd' AddMonoid.toAddAction VAddAssocClass.left instFunLikeAddActionHom conjMap	—	VAddAssocClass.left
conjMap_bijective 📖	mathematical	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	Function.Bijective SubAddAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddAction.stabilizer AddSubgroup.toAddGroup AddSubgroup.instAddAction SubAddAction.instSetLike SubAddAction.ofStabilizer DFunLike.coe AddActionHom AddEquiv AddSubgroup.add EquivLike.toFunLike AddEquiv.instEquivLike AddAction.stabilizerEquivStabilizer SubAddAction.vadd' AddMonoid.toAddAction VAddAssocClass.left instFunLikeAddActionHom conjMap	—	VAddAssocClass.left AddAction.injective conjMap_apply SetLike.coe_eq_coe eq_neg_vadd_iff neg_conjMap_comp_apply
conjMap_comp 📖	mathematical	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	AddActionHom.comp AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddAction.stabilizer DFunLike.coe AddEquiv AddSubgroup.add EquivLike.toFunLike AddEquiv.instEquivLike AddAction.stabilizerEquivStabilizer SubAddAction AddSubgroup.toAddGroup AddSubgroup.instAddAction SubAddAction.instSetLike SubAddAction.ofStabilizer SubAddAction.vadd' AddMonoid.toAddAction VAddAssocClass.left conjMap AddAction.stabilizerEquivStabilizer_compTriple	—	AddActionHom.ext VAddAssocClass.left AddAction.stabilizerEquivStabilizer_compTriple SetLike.coe_eq_coe conjMap_comp_apply
conjMap_comp_apply 📖	mathematical	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	DFunLike.coe AddActionHom AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddAction.stabilizer AddEquiv AddSubgroup.add EquivLike.toFunLike AddEquiv.instEquivLike AddAction.stabilizerEquivStabilizer SubAddAction AddSubgroup.toAddGroup AddSubgroup.instAddAction SubAddAction.instSetLike SubAddAction.ofStabilizer SubAddAction.vadd' AddMonoid.toAddAction VAddAssocClass.left instFunLikeAddActionHom conjMap	—	VAddAssocClass.left AddSemigroupAction.add_vadd
conjMap_comp_neg_apply 📖	mathematical	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	DFunLike.coe AddActionHom AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddAction.stabilizer AddEquiv AddSubgroup.add EquivLike.toFunLike AddEquiv.instEquivLike AddAction.stabilizerEquivStabilizer SubNegMonoid.toNeg eq_neg_vadd_iff SubAddAction AddSubgroup.toAddGroup AddSubgroup.instAddAction SubAddAction.instSetLike SubAddAction.ofStabilizer SubAddAction.vadd' AddMonoid.toAddAction VAddAssocClass.left instFunLikeAddActionHom conjMap	—	eq_neg_vadd_iff VAddAssocClass.left neg_vadd_vadd
neg_conjMap_comp_apply 📖	mathematical	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	DFunLike.coe AddActionHom AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddAction.stabilizer AddEquiv AddSubgroup.add EquivLike.toFunLike AddEquiv.instEquivLike AddAction.stabilizerEquivStabilizer SubAddAction AddSubgroup.toAddGroup AddSubgroup.instAddAction SubAddAction.instSetLike SubAddAction.ofStabilizer SubAddAction.vadd' AddMonoid.toAddAction VAddAssocClass.left instFunLikeAddActionHom conjMap SubNegMonoid.toNeg eq_neg_vadd_iff	—	VAddAssocClass.left eq_neg_vadd_iff vadd_neg_vadd
snoc_castSucc 📖	mathematical	—	DFunLike.coe Function.Embedding Function.instFunLikeEmbedding snoc SubAddAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddAction.stabilizer AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.toAddSemigroupAction AddSubgroup.instAddAction SubAddAction.instSetLike SubAddAction.ofStabilizer	—	Fin.snoc_castSucc
snoc_last 📖	mathematical	—	DFunLike.coe Function.Embedding Function.instFunLikeEmbedding snoc	—	Fin.snoc_last

SubMulAction

Definitions

Name	Category	Theorems
ofStabilizer 📖	CompOp	26 math math: ofStabilizer.isPretransitive_iff_of_conj, ofStabilizer.conjMap_comp_apply, ofStabilizer_carrier, ofStabilizer.conjMap_comp_inv_apply, nat_card_ofStabilizer_add_one_eq, ofStabilizer.inv_conjMap_comp_apply, ofStabilizer.isMultiplyPretransitive_iff, ofStabilizer.isPretransitive_iff, fixingSubgroup_of_insert, ofStabilizer.isMultiplyPretransitive_iff_of_conj, nat_card_ofStabilizer_eq, MulAction.isPreprimitive_fixingSubgroup_insert_iff, nat_card_ofStabilizer_eq_add_one, ENat_card_ofStabilizer_add_one_eq, notMem_val_image, mem_ofStabilizer_iff, ofStabilizer.snoc_castSucc, mem_ofFixingSubgroup_insert_iff, MulAction.isMultiplyPreprimitive_succ_iff_ofStabilizer, ofStabilizer.conjMap_comp, ofStabilizer.isMultiplyPretransitive, ofFixingSubgroup_of_singleton_bijective, MulAction.isMultiplyPreprimitive_ofStabilizer, ofStabilizer.conjMap_bijective, ofStabilizer.conjMap_apply, ofFixingSubgroup_insert_map_bijective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ENat_card_ofStabilizer_add_one_eq 📖	mathematical	—	ENat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat ENat.card SubMulAction Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction instSetLike ofStabilizer AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Cardinal.mk_sum_compl map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass OrderRingHom.instRingHomClass add_comm Cardinal.mk_fintype Fintype.card_unique Nat.cast_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
exists_smul_of_last_eq 📖	mathematical	—	Function.Embedding Function.Embedding.smul ofStabilizer.snoc	—	MulAction.exists_smul_eq Function.instEmbeddingLikeEmbedding Function.Embedding.ext Fin.eq_castSucc_or_eq_last Fin.snoc_castSucc Function.Embedding.codRestrict_apply Fin.Embedding.snoc_last
mem_ofStabilizer_iff 📖	mathematical	—	SubMulAction Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction instSetLike ofStabilizer	—	—
nat_card_ofStabilizer_add_one_eq 📖	mathematical	—	Nat.card SubMulAction Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction instSetLike ofStabilizer	—	Nat.subtype_card Finset.card_singleton Finset.card_compl_add_card Nat.card_eq_fintype_card
nat_card_ofStabilizer_eq 📖	mathematical	—	Nat.card SubMulAction Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction instSetLike ofStabilizer	—	nat_card_ofStabilizer_add_one_eq
nat_card_ofStabilizer_eq_add_one 📖	mathematical	—	Nat.card SubMulAction Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction instSetLike ofStabilizer	—	nat_card_ofStabilizer_add_one_eq
neq_of_mem_ofStabilizer 📖	—	—	—	—	Subtype.prop
notMem_val_image 📖	mathematical	—	Set Set.instMembership Set.image SubMulAction Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction instSetLike ofStabilizer	—	Subtype.prop
ofStabilizer_carrier 📖	mathematical	—	carrier Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction ofStabilizer Compl.compl Set Set.instCompl Set.instSingletonSet	—	—

SubMulAction.ofStabilizer

Definitions

Name	Category	Theorems
conjMap 📖	CompOp	6 math math: conjMap_comp_apply, conjMap_comp_inv_apply, inv_conjMap_comp_apply, conjMap_comp, conjMap_bijective, conjMap_apply
snoc 📖	CompOp	3 math math: SubMulAction.exists_smul_of_last_eq, snoc_last, snoc_castSucc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conjMap_apply 📖	mathematical	SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	SubMulAction Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Subgroup.toGroup Subgroup.instMulAction SubMulAction.instSetLike SubMulAction.ofStabilizer DFunLike.coe MulActionHom MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulAction.stabilizerEquivStabilizer SubMulAction.smul' Monoid.toMulAction IsScalarTower.left instFunLikeMulActionHom conjMap	—	IsScalarTower.left
conjMap_bijective 📖	mathematical	SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	Function.Bijective SubMulAction Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Subgroup.toGroup Subgroup.instMulAction SubMulAction.instSetLike SubMulAction.ofStabilizer DFunLike.coe MulActionHom MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulAction.stabilizerEquivStabilizer SubMulAction.smul' Monoid.toMulAction IsScalarTower.left instFunLikeMulActionHom conjMap	—	IsScalarTower.left MulAction.injective conjMap_apply SetLike.coe_eq_coe eq_inv_smul_iff inv_conjMap_comp_apply
conjMap_comp 📖	mathematical	SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	MulActionHom.comp Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer DFunLike.coe MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulAction.stabilizerEquivStabilizer SubMulAction Subgroup.toGroup Subgroup.instMulAction SubMulAction.instSetLike SubMulAction.ofStabilizer SubMulAction.smul' Monoid.toMulAction IsScalarTower.left conjMap MulAction.stabilizerEquivStabilizer_compTriple	—	MulActionHom.ext IsScalarTower.left MulAction.stabilizerEquivStabilizer_compTriple conjMap_comp_apply
conjMap_comp_apply 📖	mathematical	SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	DFunLike.coe MulActionHom Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulAction.stabilizerEquivStabilizer SubMulAction Subgroup.toGroup Subgroup.instMulAction SubMulAction.instSetLike SubMulAction.ofStabilizer SubMulAction.smul' Monoid.toMulAction IsScalarTower.left instFunLikeMulActionHom conjMap	—	IsScalarTower.left SemigroupAction.mul_smul
conjMap_comp_inv_apply 📖	mathematical	SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	DFunLike.coe MulActionHom Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulAction.stabilizerEquivStabilizer DivInvMonoid.toInv eq_inv_smul_iff SubMulAction Subgroup.toGroup Subgroup.instMulAction SubMulAction.instSetLike SubMulAction.ofStabilizer SubMulAction.smul' Monoid.toMulAction IsScalarTower.left instFunLikeMulActionHom conjMap	—	eq_inv_smul_iff IsScalarTower.left inv_smul_smul
inv_conjMap_comp_apply 📖	mathematical	SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	DFunLike.coe MulActionHom Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulAction.stabilizerEquivStabilizer SubMulAction Subgroup.toGroup Subgroup.instMulAction SubMulAction.instSetLike SubMulAction.ofStabilizer SubMulAction.smul' Monoid.toMulAction IsScalarTower.left instFunLikeMulActionHom conjMap DivInvMonoid.toInv eq_inv_smul_iff	—	IsScalarTower.left eq_inv_smul_iff smul_inv_smul
snoc_castSucc 📖	mathematical	—	DFunLike.coe Function.Embedding Function.instFunLikeEmbedding snoc SubMulAction Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction SubMulAction.instSetLike SubMulAction.ofStabilizer	—	Fin.snoc_castSucc
snoc_last 📖	mathematical	—	DFunLike.coe Function.Embedding Function.instFunLikeEmbedding snoc	—	Fin.snoc_last

VAdd

Definitions

Name	Category	Theorems
ofStabilizer 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
instAddActionSubtypeMemAddSubgroupStabilizerSetElem 📖	CompOp	—
instMulActionSubtypeMemSubgroupStabilizerSetElem 📖	CompOp	2 math math: alternatingGroup.stabilizer.surjective_toPerm, Equiv.Perm.stabilizer.surjective_toPerm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
stabilizer_compl 📖	mathematical	—	MulAction.stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid Compl.compl Set.instCompl	—	Set.smul_set_compl MulAction.mem_stabilizer_iff le_antisymm compl_compl
stabilizer_empty_eq_top 📖	mathematical	—	MulAction.stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid Set.instEmptyCollection Top.top Subgroup Subgroup.instTop	—	Subgroup.ext Set.smul_set_empty
stabilizer_univ_eq_top 📖	mathematical	—	MulAction.stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid Set.univ Top.top Subgroup Subgroup.instTop	—	Subgroup.ext Set.smul_set_univ

---

← Back to Index