FixingSubgroup

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

Statistics

Metric	Count
Definitions fixingAddSubgroup, fixingAddSubmonoid, fixingSubgroup, fixingSubmonoid	4
Theorems fixedPoints_addSubgroup_antitone, fixedPoints_addSubgroup_iSup, fixedPoints_addSubgroup_sup, fixedPoints_addSubmonoid_iSup, fixedPoints_addSubmonoid_sup, fixedPoints_antitone, fixedPoints_antitone_addSubmonoid, fixedPoints_subgroup_antitone, fixedPoints_subgroup_iSup, fixedPoints_subgroup_sup, fixedPoints_submonoid_iSup, fixedPoints_submonoid_sup, fixingAddSubgroup_antitone, fixingAddSubgroup_empty, fixingAddSubgroup_fixedPoints_gc, fixingAddSubgroup_iUnion, fixingAddSubgroup_union, fixingAddSubmonoid_antitone, fixingAddSubmonoid_fixedPoints_gc, fixingAddSubmonoid_iUnion, fixingAddSubmonoid_union, fixingSubgroup_antitone, fixingSubgroup_empty, fixingSubgroup_fixedPoints_gc, fixingSubgroup_iUnion, fixingSubgroup_union, fixingSubmonoid_antitone, fixingSubmonoid_fixedPoints_gc, fixingSubmonoid_iUnion, fixingSubmonoid_union, mem_fixingAddSubgroup_compl_iff_movedBy_subset, mem_fixingAddSubgroup_iff, mem_fixingAddSubgroup_iff_subset_fixedBy, mem_fixingAddSubmonoid_iff, mem_fixingSubgroup_compl_iff_movedBy_subset, mem_fixingSubgroup_iff, mem_fixingSubgroup_iff_subset_fixedBy, mem_fixingSubmonoid_iff, orbit_fixingAddSubgroup_compl_subset, orbit_fixingSubgroup_compl_subset	40
Total	44

(root)

Definitions

Name	Category	Theorems
fixingAddSubgroup 📖	CompOp	42 math math: SubAddAction.map_ofFixingAddSubgroupUnion_bijective, SubAddAction.ofFixingAddSubgroup_of_inclusion_injective, SubAddAction.ofFixingAddSubgroup_of_singleton_bijective, orbit_fixingAddSubgroup_compl_subset, AddAction.isPreprimitive_ofFixingAddSubgroup_conj_iff, SubAddAction.ofFixingAddSubgroup.isMultiplyPretransitive, fixingAddSubgroup_iUnion, SubAddAction.ofFixingAddSubgroup.isMultiplyPretransitive', fixingAddSubgroup_empty, SubAddAction.conjMap_ofFixingAddSubgroup_bijective, fixingAddSubgroup_union, SubAddAction.conjMap_ofFixingAddSubgroup_coe_apply, mem_fixingAddSubgroup_compl_iff_movedBy_subset, SubAddAction.ofFixingAddSubgroup_of_eq_bijective, SubAddAction.mem_fixingAddSubgroup_union_iff, SubAddAction.ofFixingAddSubgroup_insert_map_bijective, SubAddAction.fixingAddSubgroup_vadd_eq_fixingAddSubgroup_map_conj, SubAddAction.ofFixingAddSubgroup_of_eq_apply, AddAction.fixingAddSubgroup_le_stabilizer, SubAddAction.mem_fixingAddSubgroup_insert_iff, SubAddAction.fixingAddSubgroupEquivFixingAddSubgroup_coe_apply, SubAddAction.fixingAddSubgroup_of_insert, SubAddAction.of_fixingAddSubgroupEmpty_mapScalars_surjective, SubAddAction.mem_ofFixingAddSubgroup_iff, SubAddAction.ofFixingAddSubgroupEmpty_equivariantMap_bijective, fixingAddSubgroup_fixedPoints_gc, SubAddAction.ofFixingAddSubgroup_carrier, fixingAddSubgroup_antitone, AddAction.isMultiplyPreprimitive_iff, SubAddAction.ofFixingAddSubgroup.append_right, SubAddAction.ofFixingAddSubgroup_equivariantMap_injective, AddAction.ofFixingSubgroup.isMultiplyPreprimitive, AddAction.IsMultiplyPreprimitive.isPreprimitive_ofFixingAddSubgroup, SubAddAction.disjoint_val_image, SubAddAction.fixingAddSubgroup_map_conj_eq, mem_fixingAddSubgroup_iff_subset_fixedBy, AddAction.isPreprimitive_fixingAddSubgroup_insert_iff, SubAddAction.mem_ofFixingAddSubgroup_insert_iff, AddAction.isPreprimitive_of_fixingAddSubgroup_empty_iff, SubAddAction.not_mem_of_mem_ofFixingAddSubgroup, mem_fixingAddSubgroup_iff, SubAddAction.map_ofFixingAddSubgroupUnion_def
fixingAddSubmonoid 📖	CompOp	5 math math: fixingAddSubmonoid_fixedPoints_gc, mem_fixingAddSubmonoid_iff, fixingAddSubmonoid_antitone, fixingAddSubmonoid_union, fixingAddSubmonoid_iUnion
fixingSubgroup 📖	CompOp	58 math math: fixingSubgroup_union, MulAction.isPreprimitive_of_fixingSubgroup_empty_iff, fixingSubgroup_antitone, SubMulAction.ofFixingSubgroup_equivariantMap_injective, SubMulAction.fixingSubgroup_smul_eq_fixingSubgroup_map_conj, IsGaloisGroup.fixingSubgroup_top, SubMulAction.ofFixingSubgroup_of_inclusion_injective, fixingSubgroup_empty, SubMulAction.map_ofFixingSubgroupUnion_def, MulAction.ofFixingSubgroup.isMultiplyPreprimitive, SubMulAction.fixingSubgroup_of_insert, SubMulAction.ofFixingSubgroup_carrier, MulAction.isPreprimitive_ofFixingSubgroup_conj_iff, IsGaloisGroup.fixedPoints_fixingSubgroup, SubMulAction.mem_fixingSubgroup_insert_iff, IsGaloisGroup.le_fixedPoints_iff_le_fixingSubgroup, IsGaloisGroup.fixingSubgroup_le_of_le, SubMulAction.disjoint_val_image, IsGaloisGroup.fixingSubgroup_fixedPoints, IsGaloisGroup.ofDual_intermediateFieldEquivSubgroup_apply, MulAction.isPreprimitive_fixingSubgroup_insert_iff, SubMulAction.ofFixingSubgroup_of_eq_apply, mem_fixingSubgroup_compl_iff_movedBy_subset, SubMulAction.ofFixingSubgroup.isMultiplyPretransitive, MulAction.IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup, MulAction.isMultiplyPreprimitive_iff, SubMulAction.mem_ofFixingSubgroup_insert_iff, Equiv.Perm.isPretransitive_of_isCycle_mem, MulAction.IsMultiplyPretransitive.index_of_fixingSubgroup_eq, fixingSubgroup_iUnion, IsGaloisGroup.intermediateField, SubMulAction.ofFixingSubgroup.append_right, SubMulAction.fixingSubgroup_map_conj_eq, IsGaloisGroup.fixingSubgroup_bot, IsGaloisGroup.intermediateFieldEquivSubgroup_apply, SubMulAction.ofFixingSubgroup_of_singleton_bijective, SubMulAction.ofFixingSubgroupEmpty_equivariantMap_bijective, SubMulAction.fixingSubgroupEquivFixingSubgroup_coe_apply, SubMulAction.mem_fixingSubgroup_union_iff, fixingSubgroup_fixedPoints_gc, SubMulAction.map_ofFixingSubgroupUnion_bijective, SubMulAction.of_fixingSubgroupEmpty_mapScalars_surjective, SubMulAction.ofFixingSubgroup_of_eq_bijective, SubMulAction.not_mem_of_mem_ofFixingSubgroup, SubMulAction.IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter, MulAction.fixingSubgroup_le_stabilizer, mem_fixingSubgroup_iff_subset_fixedBy, SubMulAction.mem_ofFixingSubgroup_iff, mem_fixingSubgroup_iff, SubMulAction.ofFixingSubgroup.isMultiplyPretransitive', IsGaloisGroup.card_fixingSubgroup_eq_finrank, SubMulAction.ofFixingSubgroup_insert_map_bijective, SubMulAction.conjMap_ofFixingSubgroup_bijective, IsGaloisGroup.map_mulEquivAlgEquiv_fixingSubgroup, orbit_fixingSubgroup_compl_subset, SubMulAction.IsPretransitive.isPretransitive_ofFixingSubgroup_inter, SubMulAction.conjMap_ofFixingSubgroup_coe_apply, MulAction.IsMultiplyPretransitive.index_of_fixingSubgroup_mul
fixingSubmonoid 📖	CompOp	5 math math: fixingSubmonoid_antitone, fixingSubmonoid_union, fixingSubmonoid_fixedPoints_gc, fixingSubmonoid_iUnion, mem_fixingSubmonoid_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fixedPoints_addSubgroup_antitone 📖	mathematical	—	Antitone AddSubgroup Set PartialOrder.toPreorder AddSubgroup.instPartialOrder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra AddAction.fixedPoints SetLike.instMembership AddSubgroup.instSetLike SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.instAddAction	—	Monotone.dual_left GaloisConnection.monotone_u fixingAddSubgroup_fixedPoints_gc
fixedPoints_addSubgroup_iSup 📖	mathematical	—	AddAction.fixedPoints AddSubgroup SetLike.instMembership AddSubgroup.instSetLike iSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup AddSubgroup.instCompleteLattice SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.instAddAction Set.iInter	—	GaloisConnection.u_iInf fixingAddSubgroup_fixedPoints_gc
fixedPoints_addSubgroup_sup 📖	mathematical	—	AddAction.fixedPoints AddSubgroup SetLike.instMembership AddSubgroup.instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice AddSubgroup.instCompleteLattice SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.instAddAction Set Set.instInter	—	GaloisConnection.u_inf fixingAddSubgroup_fixedPoints_gc
fixedPoints_addSubmonoid_iSup 📖	mathematical	—	AddAction.fixedPoints AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership AddSubmonoid.instSetLike iSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup AddSubmonoid.instCompleteLattice AddSubmonoid.toAddMonoid AddSubmonoid.addAction Set.iInter	—	GaloisConnection.u_iInf fixingAddSubmonoid_fixedPoints_gc
fixedPoints_addSubmonoid_sup 📖	mathematical	—	AddAction.fixedPoints AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership AddSubmonoid.instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice AddSubmonoid.instCompleteLattice AddSubmonoid.toAddMonoid AddSubmonoid.addAction Set Set.instInter	—	GaloisConnection.u_inf fixingAddSubmonoid_fixedPoints_gc
fixedPoints_antitone 📖	mathematical	—	Antitone Submonoid Monoid.toMulOneClass Set PartialOrder.toPreorder Submonoid.instPartialOrder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra MulAction.fixedPoints SetLike.instMembership Submonoid.instSetLike Submonoid.toMonoid Submonoid.mulAction	—	Monotone.dual_left GaloisConnection.monotone_u fixingSubmonoid_fixedPoints_gc
fixedPoints_antitone_addSubmonoid 📖	mathematical	—	Antitone AddSubmonoid AddMonoid.toAddZeroClass Set PartialOrder.toPreorder AddSubmonoid.instPartialOrder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra AddAction.fixedPoints SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.toAddMonoid AddSubmonoid.addAction	—	Monotone.dual_left GaloisConnection.monotone_u fixingAddSubmonoid_fixedPoints_gc
fixedPoints_subgroup_antitone 📖	mathematical	—	Antitone Subgroup Set PartialOrder.toPreorder Subgroup.instPartialOrder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra MulAction.fixedPoints SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.instMulAction	—	Monotone.dual_left GaloisConnection.monotone_u fixingSubgroup_fixedPoints_gc
fixedPoints_subgroup_iSup 📖	mathematical	—	MulAction.fixedPoints Subgroup SetLike.instMembership Subgroup.instSetLike iSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup Subgroup.instCompleteLattice DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.instMulAction Set.iInter	—	GaloisConnection.u_iInf fixingSubgroup_fixedPoints_gc
fixedPoints_subgroup_sup 📖	mathematical	—	MulAction.fixedPoints Subgroup SetLike.instMembership Subgroup.instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice Subgroup.instCompleteLattice DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.instMulAction Set Set.instInter	—	GaloisConnection.u_inf fixingSubgroup_fixedPoints_gc
fixedPoints_submonoid_iSup 📖	mathematical	—	MulAction.fixedPoints Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike iSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup Submonoid.instCompleteLattice Submonoid.toMonoid Submonoid.mulAction Set.iInter	—	GaloisConnection.u_iInf fixingSubmonoid_fixedPoints_gc
fixedPoints_submonoid_sup 📖	mathematical	—	MulAction.fixedPoints Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice Submonoid.instCompleteLattice Submonoid.toMonoid Submonoid.mulAction Set Set.instInter	—	GaloisConnection.u_inf fixingSubmonoid_fixedPoints_gc
fixingAddSubgroup_antitone 📖	mathematical	—	Antitone Set AddSubgroup PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra AddSubgroup.instPartialOrder fixingAddSubgroup	—	GaloisConnection.monotone_l fixingAddSubgroup_fixedPoints_gc
fixingAddSubgroup_empty 📖	mathematical	—	fixingAddSubgroup Set Set.instEmptyCollection Top.top AddSubgroup AddSubgroup.instTop	—	GaloisConnection.l_bot fixingAddSubgroup_fixedPoints_gc
fixingAddSubgroup_fixedPoints_gc 📖	mathematical	—	GaloisConnection Set OrderDual AddSubgroup PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra OrderDual.instPreorder AddSubgroup.instPartialOrder DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual fixingAddSubgroup AddAction.fixedPoints SetLike.instMembership AddSubgroup.instSetLike SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.instAddAction OrderDual.ofDual	—	—
fixingAddSubgroup_iUnion 📖	mathematical	—	fixingAddSubgroup Set.iUnion iInf AddSubgroup AddSubgroup.instInfSet	—	GaloisConnection.l_iSup fixingAddSubgroup_fixedPoints_gc
fixingAddSubgroup_union 📖	mathematical	—	fixingAddSubgroup Set Set.instUnion AddSubgroup AddSubgroup.instMin	—	GaloisConnection.l_sup fixingAddSubgroup_fixedPoints_gc
fixingAddSubmonoid_antitone 📖	mathematical	—	Antitone Set AddSubmonoid AddMonoid.toAddZeroClass PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra AddSubmonoid.instPartialOrder fixingAddSubmonoid	—	GaloisConnection.monotone_l fixingAddSubmonoid_fixedPoints_gc
fixingAddSubmonoid_fixedPoints_gc 📖	mathematical	—	GaloisConnection Set OrderDual AddSubmonoid AddMonoid.toAddZeroClass PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra OrderDual.instPreorder AddSubmonoid.instPartialOrder DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual fixingAddSubmonoid AddAction.fixedPoints SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.toAddMonoid AddSubmonoid.addAction OrderDual.ofDual	—	—
fixingAddSubmonoid_iUnion 📖	mathematical	—	fixingAddSubmonoid Set.iUnion iInf AddSubmonoid AddMonoid.toAddZeroClass AddSubmonoid.instInfSet	—	GaloisConnection.l_iSup fixingAddSubmonoid_fixedPoints_gc
fixingAddSubmonoid_union 📖	mathematical	—	fixingAddSubmonoid Set Set.instUnion AddSubmonoid AddMonoid.toAddZeroClass AddSubmonoid.instMin	—	GaloisConnection.l_sup fixingAddSubmonoid_fixedPoints_gc
fixingSubgroup_antitone 📖	mathematical	—	Antitone Set Subgroup PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Subgroup.instPartialOrder fixingSubgroup	—	GaloisConnection.monotone_l fixingSubgroup_fixedPoints_gc
fixingSubgroup_empty 📖	mathematical	—	fixingSubgroup Set Set.instEmptyCollection Top.top Subgroup Subgroup.instTop	—	GaloisConnection.l_bot fixingSubgroup_fixedPoints_gc
fixingSubgroup_fixedPoints_gc 📖	mathematical	—	GaloisConnection Set OrderDual Subgroup PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra OrderDual.instPreorder Subgroup.instPartialOrder DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual fixingSubgroup MulAction.fixedPoints SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.instMulAction OrderDual.ofDual	—	—
fixingSubgroup_iUnion 📖	mathematical	—	fixingSubgroup Set.iUnion iInf Subgroup Subgroup.instInfSet	—	GaloisConnection.l_iSup fixingSubgroup_fixedPoints_gc
fixingSubgroup_union 📖	mathematical	—	fixingSubgroup Set Set.instUnion Subgroup Subgroup.instMin	—	GaloisConnection.l_sup fixingSubgroup_fixedPoints_gc
fixingSubmonoid_antitone 📖	mathematical	—	Antitone Set Submonoid Monoid.toMulOneClass PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Submonoid.instPartialOrder fixingSubmonoid	—	GaloisConnection.monotone_l fixingSubmonoid_fixedPoints_gc
fixingSubmonoid_fixedPoints_gc 📖	mathematical	—	GaloisConnection Set OrderDual Submonoid Monoid.toMulOneClass PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra OrderDual.instPreorder Submonoid.instPartialOrder DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual fixingSubmonoid MulAction.fixedPoints SetLike.instMembership Submonoid.instSetLike Submonoid.toMonoid Submonoid.mulAction OrderDual.ofDual	—	—
fixingSubmonoid_iUnion 📖	mathematical	—	fixingSubmonoid Set.iUnion iInf Submonoid Monoid.toMulOneClass Submonoid.instInfSet	—	GaloisConnection.l_iSup fixingSubmonoid_fixedPoints_gc
fixingSubmonoid_union 📖	mathematical	—	fixingSubmonoid Set Set.instUnion Submonoid Monoid.toMulOneClass Submonoid.instMin	—	GaloisConnection.l_sup fixingSubmonoid_fixedPoints_gc
mem_fixingAddSubgroup_compl_iff_movedBy_subset 📖	mathematical	—	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup Compl.compl Set Set.instCompl Set.instHasSubset AddAction.fixedBy SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	mem_fixingAddSubgroup_iff_subset_fixedBy Set.compl_subset_comm
mem_fixingAddSubgroup_iff 📖	mathematical	—	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	—	—
mem_fixingAddSubgroup_iff_subset_fixedBy 📖	mathematical	—	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup Set Set.instHasSubset AddAction.fixedBy SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	mem_fixingAddSubgroup_iff AddAction.mem_fixedBy
mem_fixingAddSubmonoid_iff 📖	mathematical	—	AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership AddSubmonoid.instSetLike fixingAddSubmonoid HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction	—	—
mem_fixingSubgroup_compl_iff_movedBy_subset 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup Compl.compl Set Set.instCompl Set.instHasSubset MulAction.fixedBy DivInvMonoid.toMonoid Group.toDivInvMonoid	—	mem_fixingSubgroup_iff_subset_fixedBy Set.compl_subset_comm
mem_fixingSubgroup_iff 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	—
mem_fixingSubgroup_iff_subset_fixedBy 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup Set Set.instHasSubset MulAction.fixedBy DivInvMonoid.toMonoid Group.toDivInvMonoid	—	—
mem_fixingSubmonoid_iff 📖	mathematical	—	Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike fixingSubmonoid SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	—
orbit_fixingAddSubgroup_compl_subset 📖	mathematical	Set Set.instMembership	Set.instHasSubset AddAction.orbit AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup Compl.compl Set.instCompl AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.toAddSemigroupAction AddAction.instAddAction	—	AddAction.mem_orbit_iff AddSubmonoid.mk_vadd AddAction.vadd_mem_of_set_mem_fixedBy AddAction.set_mem_fixedBy_of_movedBy_subset mem_fixingAddSubgroup_compl_iff_movedBy_subset
orbit_fixingSubgroup_compl_subset 📖	mathematical	Set Set.instMembership	Set.instHasSubset MulAction.orbit Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup Compl.compl Set.instCompl SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction MulAction.instMulAction	—	MulAction.mem_orbit_iff Submonoid.mk_smul MulAction.smul_mem_of_set_mem_fixedBy MulAction.set_mem_fixedBy_of_movedBy_subset mem_fixingSubgroup_compl_iff_movedBy_subset

---

← Back to Index