Basic

📁 Source: Mathlib/GroupTheory/GroupAction/Basic.lean

Statistics

Metric	Count
Definitions instDecidablePredMemSetFixedByAddOfDecidableEq, stabilizerEquivStabilizer, stabilizerEquivStabilizerOfOrbitRel, instDecidablePredMemSetFixedByOfDecidableEq, stabilizerEquivStabilizer, stabilizerEquivStabilizerOfOrbitRel	6
Theorems fixedPoints_of_subsingleton, fst_mem_orbit_of_mem_orbit, instIsPretransitiveElemOrbit, instIsPretransitiveElemOrbit_1, le_stabilizer_iff_vadd_le, mem_fixedPoints_iff_card_orbit_eq_one, nontrivial_of_fixedPoints_ne_univ, orbitRel_addSubgroupOf, orbitRel_addSubgroup_le, orbitRel_le_fst, orbitRel_le_snd, orbit_eq_univ, pretransitive_iff_subsingleton_quotient, pretransitive_iff_unique_quotient_of_nonempty, snd_mem_orbit_of_mem_orbit, stabilizerEquivStabilizer_apply, stabilizerEquivStabilizer_neg, stabilizerEquivStabilizer_symm, stabilizerEquivStabilizer_symm_apply, stabilizerEquivStabilizer_trans, stabilizerEquivStabilizer_zero, stabilizer_vadd_eq_stabilizer_map_conj, subsingleton_orbit_iff_mem_fixedPoints, vadd_orbit, swap_mem_stabilizer, finite_addAction_orbit, finite_mulAction_orbit, of_finite_addAction_orbitRel_quotient, of_finite_mulAction_orbitRel_quotient, stabilizer_eq_bot, stabilizer_eq_bot, stabilizer_units_eq_bot_of_ne_zero, fixedPoints_of_subsingleton, fst_mem_orbit_of_mem_orbit, instIsPretransitiveElemOrbit, instIsPretransitiveElemOrbit_1, le_stabilizer_iff_smul_le, mem_fixedPoints_iff_card_orbit_eq_one, nontrivial_of_fixedPoints_ne_univ, orbitRel_le_fst, orbitRel_le_snd, orbitRel_subgroupOf, orbitRel_subgroup_le, orbit_eq_univ, pretransitive_iff_subsingleton_quotient, pretransitive_iff_unique_quotient_of_nonempty, smul_orbit, snd_mem_orbit_of_mem_orbit, stabilizerEquivStabilizer_apply, stabilizerEquivStabilizer_inv, stabilizerEquivStabilizer_one, stabilizerEquivStabilizer_symm, stabilizerEquivStabilizer_symm_apply, stabilizerEquivStabilizer_trans, stabilizer_smul_eq_stabilizer_map_conj, subsingleton_orbit_iff_mem_fixedPoints, isCancelSMul_iff_stabilizer_eq_bot, isCancelVAdd_iff_stabilizer_eq_bot, smul_cancel_of_non_zero_divisor	59
Total	65

AddAction

Definitions

Name	Category	Theorems
instDecidablePredMemSetFixedByAddOfDecidableEq 📖	CompOp	—
stabilizerEquivStabilizer 📖	CompOp	13 math math: stabilizerEquivStabilizer_symm, SubAddAction.ofStabilizer.conjMap_comp, SubAddAction.ofStabilizer.conjMap_comp_neg_apply, stabilizerEquivStabilizer_symm_apply, stabilizerEquivStabilizer_neg, SubAddAction.ofStabilizer.conjMap_bijective, stabilizerEquivStabilizer_apply, stabilizerEquivStabilizer_trans, SubAddAction.ofStabilizer.neg_conjMap_comp_apply, SubAddAction.ofStabilizer.conjMap_comp_apply, stabilizerEquivStabilizer_zero, stabilizerEquivStabilizer_compTriple, SubAddAction.ofStabilizer.conjMap_apply
stabilizerEquivStabilizerOfOrbitRel 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fixedPoints_of_subsingleton 📖	mathematical	—	fixedPoints SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Set.univ	—	Set.eq_univ_of_forall mem_fixedPoints
fst_mem_orbit_of_mem_orbit 📖	—	Set Set.instMembership orbit Prod.instVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction	—	—	mem_orbit
instIsPretransitiveElemOrbit 📖	mathematical	—	IsPretransitive Set.Elem orbit AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddSemigroupAction instElemOrbit	—	AddSemigroupAction.add_vadd neg_vadd_vadd
instIsPretransitiveElemOrbit_1 📖	mathematical	—	IsPretransitive Set.Elem orbitRel.Quotient.orbit AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddSemigroupAction instElemOrbit_1	—	Quotient.inductionOn' Quotient.eq'' orbitRel.Quotient.mem_orbit AddSemigroupAction.add_vadd neg_vadd_vadd
le_stabilizer_iff_vadd_le 📖	mathematical	—	AddSubgroup Preorder.toLE PartialOrder.toPreorder AddSubgroup.instPartialOrder stabilizer Set Set.addActionSet SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Set.instHasSubset HVAdd.hVAdd instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction	—	Eq.subset Set.instReflSubset mem_stabilizer_iff subset_antisymm Set.instAntisymmSubset NegMemClass.neg_mem AddSubgroupClass.toNegMemClass AddSubgroup.instAddSubgroupClass Set.vadd_mem_vadd_set_iff vadd_neg_vadd
mem_fixedPoints_iff_card_orbit_eq_one 📖	mathematical	—	Set Set.instMembership fixedPoints Fintype.card Set.Elem orbit AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction	—	subsingleton_orbit_iff_mem_fixedPoints le_antisymm_iff Fintype.card_le_one_iff_subsingleton Set.subsingleton_coe Fintype.card_pos_iff Set.nonempty_coe_sort nonempty_orbit
nontrivial_of_fixedPoints_ne_univ 📖	mathematical	—	Nontrivial	—	subsingleton_or_nontrivial fixedPoints_of_subsingleton
orbitRel_addSubgroupOf 📖	mathematical	—	orbitRel AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.toAddGroup AddSubgroup.addSubgroupOf instAddAction AddSubgroup.instMin	—	AddSubgroup.addSubgroupOf_map_subtype Setoid.ext orbitRel_apply mem_orbit AddSubgroup.mem_inf SetLike.coe_mem AddSubgroup.mem_addSubgroupOf
orbitRel_addSubgroup_le 📖	mathematical	—	Setoid.instLE_mathlib orbitRel AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.toAddGroup instAddAction	—	Setoid.le_def mem_orbit_of_mem_orbit_addSubgroup
orbitRel_le_fst 📖	mathematical	—	Setoid.instLE_mathlib orbitRel Prod.addAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Setoid.comap	—	Setoid.le_def fst_mem_orbit_of_mem_orbit
orbitRel_le_snd 📖	mathematical	—	Setoid.instLE_mathlib orbitRel Prod.addAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Setoid.comap	—	Setoid.le_def snd_mem_orbit_of_mem_orbit
orbit_eq_univ 📖	mathematical	—	orbit AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction Set.univ	—	Function.Surjective.range_eq surjective_vadd
pretransitive_iff_subsingleton_quotient 📖	mathematical	—	IsPretransitive AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddSemigroupAction orbitRel.Quotient	—	exists_vadd_eq Quotient.eq''
pretransitive_iff_unique_quotient_of_nonempty 📖	mathematical	—	IsPretransitive AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddSemigroupAction Unique orbitRel.Quotient	—	unique_iff_subsingleton_and_nonempty pretransitive_iff_subsingleton_quotient nonempty_quotient_iff
snd_mem_orbit_of_mem_orbit 📖	—	Set Set.instMembership orbit Prod.instVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction	—	—	mem_orbit
stabilizerEquivStabilizer_apply 📖	mathematical	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddSemigroupAction	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike stabilizer DFunLike.coe AddEquiv AddSubgroup.add EquivLike.toFunLike AddEquiv.instEquivLike stabilizerEquivStabilizer AddSemigroup.toAdd Equiv Additive AddAut Equiv.instEquivLike Additive.toMul AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass Additive.addZeroClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AddAut.instGroup AddMonoidHom.instFunLike AddAut.conj	—	—
stabilizerEquivStabilizer_neg 📖	mathematical	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddSemigroupAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	stabilizerEquivStabilizer AddEquiv.symm AddSubgroup SetLike.instMembership AddSubgroup.instSetLike stabilizer AddSubgroup.add SubNegMonoid.toNeg neg_vadd_eq_iff	—	AddEquiv.ext neg_vadd_eq_iff map_neg AddMonoidHom.instAddMonoidHomClass
stabilizerEquivStabilizer_symm 📖	mathematical	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddSemigroupAction	AddEquiv.symm AddSubgroup SetLike.instMembership AddSubgroup.instSetLike stabilizer AddSubgroup.add stabilizerEquivStabilizer SubNegMonoid.toNeg eq_neg_vadd_iff	—	AddEquiv.ext eq_neg_vadd_iff map_neg AddMonoidHom.instAddMonoidHomClass
stabilizerEquivStabilizer_symm_apply 📖	mathematical	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddSemigroupAction	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike stabilizer DFunLike.coe AddEquiv AddSubgroup.add EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm stabilizerEquivStabilizer AddSemigroup.toAdd Equiv Additive AddAut Equiv.instEquivLike Additive.toMul AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass Additive.addZeroClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AddAut.instGroup AddMonoidHom.instFunLike AddAut.conj NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	map_neg AddMonoidHom.instAddMonoidHomClass
stabilizerEquivStabilizer_trans 📖	mathematical	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddSemigroupAction AddSemigroup.toAdd	AddEquiv.trans AddSubgroup SetLike.instMembership AddSubgroup.instSetLike stabilizer AddSubgroup.add stabilizerEquivStabilizer	—	AddEquiv.ext stabilizerEquivStabilizer_apply stabilizerEquivStabilizer.congr_simp map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass
stabilizerEquivStabilizer_zero 📖	mathematical	—	stabilizerEquivStabilizer AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction zero_vadd AddEquiv.refl AddSubgroup SetLike.instMembership AddSubgroup.instSetLike stabilizer AddSubgroup.add	—	AddEquiv.ext zero_vadd stabilizerEquivStabilizer_apply map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass
stabilizer_vadd_eq_stabilizer_map_conj 📖	mathematical	—	stabilizer HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddSemigroupAction AddSubgroup.map AddEquiv.toAddMonoidHom AddMonoid.toAddZeroClass DFunLike.coe Equiv Additive AddAut AddSemigroup.toAdd EquivLike.toFunLike Equiv.instEquivLike Additive.toMul AddMonoidHom AddZeroClass.toAddZero Additive.addZeroClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AddAut.instGroup AddMonoidHom.instFunLike AddAut.conj	—	AddSubgroup.ext mem_stabilizer_iff vadd_left_cancel_iff vadd_vadd neg_add_cancel zero_vadd AddSubgroup.mem_map_equiv AddAut.conj_symm_apply
subsingleton_orbit_iff_mem_fixedPoints 📖	mathematical	—	Set.Subsingleton orbit AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction Set Set.instMembership fixedPoints	—	mem_fixedPoints mem_orbit mem_orbit_self
vadd_orbit 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddSemigroupAction orbit	—	HasSubset.Subset.antisymm Set.instAntisymmSubset vadd_orbit_subset vadd_neg_vadd Set.image_mono

Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
swap_mem_stabilizer 📖	mathematical	—	Perm Subgroup Perm.permGroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid Perm.applyMulAction swap Set.instMembership	—	MulAction.mem_stabilizer_iff Set.ext_iff swap_inv

Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_addAction_orbit 📖	mathematical	—	Set.Finite AddAction.orbit AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction	—	Set.finite_range
finite_mulAction_orbit 📖	mathematical	—	Set.Finite MulAction.orbit SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	Set.finite_range
of_finite_addAction_orbitRel_quotient 📖	mathematical	—	Finite	—	Equiv.finite_iff Quotient.inductionOn' Set.finite_coe_iff finite_addAction_orbit instSigma
of_finite_mulAction_orbitRel_quotient 📖	mathematical	—	Finite	—	Equiv.finite_iff Quotient.inductionOn' finite_mulAction_orbit instSigma

IsCancelSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
stabilizer_eq_bot 📖	mathematical	—	MulAction.stabilizer Bot.bot Subgroup Subgroup.instBot	—	Subgroup.eq_bot_iff_forall eq_one_of_smul

IsCancelVAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
stabilizer_eq_bot 📖	mathematical	—	AddAction.stabilizer Bot.bot AddSubgroup AddSubgroup.instBot	—	AddSubgroup.eq_bot_iff_forall eq_zero_of_vadd

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
stabilizer_units_eq_bot_of_ne_zero 📖	mathematical	—	MulAction.stabilizer Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Units.instGroup Units.instMulAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid toDistribMulAction Bot.bot Subgroup Subgroup.instBot	—	eq_bot_iff Units.ext sub_eq_zero smul_eq_zero_iff_left IsDomain.toIsCancelMulZero Units.val_one sub_smul one_smul sub_self

MulAction

Definitions

Name	Category	Theorems
instDecidablePredMemSetFixedByOfDecidableEq 📖	CompOp	—
stabilizerEquivStabilizer 📖	CompOp	13 math math: SubMulAction.ofStabilizer.conjMap_comp_apply, SubMulAction.ofStabilizer.conjMap_comp_inv_apply, stabilizerEquivStabilizer_symm_apply, stabilizerEquivStabilizer_trans, SubMulAction.ofStabilizer.inv_conjMap_comp_apply, stabilizerEquivStabilizer_compTriple, stabilizerEquivStabilizer_apply, SubMulAction.ofStabilizer.conjMap_comp, stabilizerEquivStabilizer_one, stabilizerEquivStabilizer_symm, SubMulAction.ofStabilizer.conjMap_bijective, stabilizerEquivStabilizer_inv, SubMulAction.ofStabilizer.conjMap_apply
stabilizerEquivStabilizerOfOrbitRel 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fixedPoints_of_subsingleton 📖	mathematical	—	fixedPoints DivInvMonoid.toMonoid Group.toDivInvMonoid Set.univ	—	Set.eq_univ_of_forall
fst_mem_orbit_of_mem_orbit 📖	—	Set Set.instMembership orbit Prod.instSMul SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction	—	—	mem_orbit
instIsPretransitiveElemOrbit 📖	mathematical	—	IsPretransitive Set.Elem orbit SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toSemigroupAction instElemOrbit	—	SemigroupAction.mul_smul inv_smul_smul
instIsPretransitiveElemOrbit_1 📖	mathematical	—	IsPretransitive Set.Elem orbitRel.Quotient.orbit SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toSemigroupAction instElemOrbit_1	—	Quotient.inductionOn' Quotient.eq'' orbitRel.Quotient.mem_orbit SemigroupAction.mul_smul inv_smul_smul
le_stabilizer_iff_smul_le 📖	mathematical	—	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid Set.instHasSubset Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction	—	Eq.subset Set.instReflSubset mem_stabilizer_iff subset_antisymm Set.instAntisymmSubset InvMemClass.inv_mem SubgroupClass.toInvMemClass Subgroup.instSubgroupClass smul_inv_smul
mem_fixedPoints_iff_card_orbit_eq_one 📖	mathematical	—	Set Set.instMembership fixedPoints Fintype.card Set.Elem orbit SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction	—	—
nontrivial_of_fixedPoints_ne_univ 📖	mathematical	—	Nontrivial	—	subsingleton_or_nontrivial fixedPoints_of_subsingleton
orbitRel_le_fst 📖	mathematical	—	Setoid.instLE_mathlib orbitRel Prod.mulAction DivInvMonoid.toMonoid Group.toDivInvMonoid Setoid.comap	—	Setoid.le_def fst_mem_orbit_of_mem_orbit
orbitRel_le_snd 📖	mathematical	—	Setoid.instLE_mathlib orbitRel Prod.mulAction DivInvMonoid.toMonoid Group.toDivInvMonoid Setoid.comap	—	Setoid.le_def snd_mem_orbit_of_mem_orbit
orbitRel_subgroupOf 📖	mathematical	—	orbitRel Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup Subgroup.subgroupOf instMulAction Subgroup.instMin	—	Subgroup.subgroupOf_map_subtype Setoid.ext mem_orbit
orbitRel_subgroup_le 📖	mathematical	—	Setoid.instLE_mathlib orbitRel Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup instMulAction	—	Setoid.le_def mem_orbit_of_mem_orbit_subgroup
orbit_eq_univ 📖	mathematical	—	orbit SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction Set.univ	—	Function.Surjective.range_eq surjective_smul
pretransitive_iff_subsingleton_quotient 📖	mathematical	—	IsPretransitive SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toSemigroupAction orbitRel.Quotient	—	exists_smul_eq Quotient.eq''
pretransitive_iff_unique_quotient_of_nonempty 📖	mathematical	—	IsPretransitive SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toSemigroupAction Unique orbitRel.Quotient	—	unique_iff_subsingleton_and_nonempty pretransitive_iff_subsingleton_quotient nonempty_quotient_iff
smul_orbit 📖	mathematical	—	Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toSemigroupAction orbit	—	HasSubset.Subset.antisymm Set.instAntisymmSubset smul_orbit_subset smul_inv_smul Set.image_mono
snd_mem_orbit_of_mem_orbit 📖	—	Set Set.instMembership orbit Prod.instSMul SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction	—	—	mem_orbit
stabilizerEquivStabilizer_apply 📖	mathematical	SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toSemigroupAction	Subgroup SetLike.instMembership Subgroup.instSetLike stabilizer DFunLike.coe MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike stabilizerEquivStabilizer MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom MulAut MulAut.instGroup MonoidHom.instFunLike MulAut.conj	—	—
stabilizerEquivStabilizer_inv 📖	mathematical	SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	stabilizerEquivStabilizer MulEquiv.symm Subgroup SetLike.instMembership Subgroup.instSetLike stabilizer Subgroup.mul DivInvMonoid.toInv inv_smul_eq_iff	—	MulEquiv.ext inv_smul_eq_iff map_inv MonoidHom.instMonoidHomClass MulAut.inv_apply
stabilizerEquivStabilizer_one 📖	mathematical	—	stabilizerEquivStabilizer MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction one_smul MulEquiv.refl Subgroup SetLike.instMembership Subgroup.instSetLike stabilizer Subgroup.mul	—	MulEquiv.ext one_smul stabilizerEquivStabilizer_apply map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass
stabilizerEquivStabilizer_symm 📖	mathematical	SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toSemigroupAction	MulEquiv.symm Subgroup SetLike.instMembership Subgroup.instSetLike stabilizer Subgroup.mul stabilizerEquivStabilizer DivInvMonoid.toInv eq_inv_smul_iff	—	MulEquiv.ext eq_inv_smul_iff map_inv MonoidHom.instMonoidHomClass MulAut.inv_apply
stabilizerEquivStabilizer_symm_apply 📖	mathematical	SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toSemigroupAction	Subgroup SetLike.instMembership Subgroup.instSetLike stabilizer DFunLike.coe MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm stabilizerEquivStabilizer MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom MulAut MulAut.instGroup MonoidHom.instFunLike MulAut.conj InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	map_inv MonoidHom.instMonoidHomClass MulAut.inv_apply
stabilizerEquivStabilizer_trans 📖	mathematical	SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toSemigroupAction MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	MulEquiv.trans Subgroup SetLike.instMembership Subgroup.instSetLike stabilizer Subgroup.mul stabilizerEquivStabilizer	—	MulEquiv.ext stabilizerEquivStabilizer_apply stabilizerEquivStabilizer.congr_simp map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass
stabilizer_smul_eq_stabilizer_map_conj 📖	mathematical	—	stabilizer SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toSemigroupAction Subgroup.map MulEquiv.toMonoidHom Monoid.toMulOneClass DFunLike.coe MonoidHom MulAut MulOne.toMul MulOneClass.toMulOne MulAut.instGroup MonoidHom.instFunLike MulAut.conj	—	Subgroup.ext mem_stabilizer_iff smul_left_cancel_iff smul_smul inv_mul_cancel one_smul Subgroup.mem_map_equiv MulAut.conj_symm_apply
subsingleton_orbit_iff_mem_fixedPoints 📖	mathematical	—	Set.Subsingleton orbit SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction Set Set.instMembership fixedPoints	—	mem_fixedPoints mem_orbit mem_orbit_self

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCancelSMul_iff_stabilizer_eq_bot 📖	mathematical	—	IsCancelSMul SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction MulAction.stabilizer Bot.bot Subgroup Subgroup.instBot	—	forall_swap
isCancelVAdd_iff_stabilizer_eq_bot 📖	mathematical	—	IsCancelVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddAction.stabilizer Bot.bot AddSubgroup AddSubgroup.instBot	—	isCancelVAdd_iff_eq_zero_of_vadd_eq forall_swap AddSubgroup.eq_bot_iff_forall AddAction.mem_stabilizer_iff
smul_cancel_of_non_zero_divisor 📖	—	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	—	sub_eq_zero smul_sub sub_self

---

← Back to Index