OfFixingSubgroup

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

Statistics

Metric	Count
Definitions instAddGroup, conjMap_ofFixingAddSubgroup, fixingAddSubgroupEquivFixingAddSubgroup, fixingAddSubgroupInsertEquiv, fixingAddSubgroup_union_to_fixingAddSubgroup_of_fixingAddSubgroup, map_ofFixingAddSubgroupUnion, ofFixingAddSubgroup, append, ofFixingAddSubgroup_equivariantMap, ofFixingAddSubgroup_insert_map, ofFixingAddSubgroup_of_eq, ofFixingAddSubgroup_of_inclusion, ofFixingAddSubgroup_of_singleton, conjMap_ofFixingSubgroup, fixingSubgroupEquivFixingSubgroup, fixingSubgroupInsertEquiv, fixingSubgroup_union_to_fixingSubgroup_of_fixingSubgroup, map_ofFixingSubgroupUnion, ofFixingSubgroup, append, ofFixingSubgroup_equivariantMap, ofFixingSubgroup_insert_map, ofFixingSubgroup_of_eq, ofFixingSubgroup_of_inclusion, ofFixingSubgroup_of_singleton	25
Theorems fixingAddSubgroup_le_stabilizer, fixingSubgroup_le_stabilizer, conj_mem_fixingAddSubgroup, conj_mem_fixingSubgroup, conjMap_ofFixingAddSubgroup_bijective, conjMap_ofFixingAddSubgroup_coe_apply, disjoint_val_image, fixingAddSubgroupEquivFixingAddSubgroup_coe_apply, fixingAddSubgroup_map_conj_eq, fixingAddSubgroup_of_insert, fixingAddSubgroup_vadd_eq_fixingAddSubgroup_map_conj, map_ofFixingAddSubgroupUnion_bijective, map_ofFixingAddSubgroupUnion_def, mem_fixingAddSubgroup_insert_iff, mem_fixingAddSubgroup_union_iff, mem_ofFixingAddSubgroup_iff, mem_ofFixingAddSubgroup_insert_iff, not_mem_of_mem_ofFixingAddSubgroup, append_left, append_right, ofFixingAddSubgroupEmpty_equivariantMap_bijective, ofFixingAddSubgroup_carrier, ofFixingAddSubgroup_equivariantMap_injective, ofFixingAddSubgroup_insert_map_apply, ofFixingAddSubgroup_insert_map_bijective, ofFixingAddSubgroup_of_eq_apply, ofFixingAddSubgroup_of_eq_bijective, ofFixingAddSubgroup_of_inclusion_injective, ofFixingAddSubgroup_of_singleton_bijective, of_fixingAddSubgroupEmpty_mapScalars_surjective, isPreprimitive_ofFixingSubgroup_inter, isPretransitive_ofFixingSubgroup_inter, conjMap_ofFixingSubgroup_bijective, conjMap_ofFixingSubgroup_coe_apply, disjoint_val_image, fixingSubgroupEquivFixingSubgroup_coe_apply, fixingSubgroup_map_conj_eq, fixingSubgroup_of_insert, fixingSubgroup_smul_eq_fixingSubgroup_map_conj, map_ofFixingSubgroupUnion_bijective, map_ofFixingSubgroupUnion_def, mem_fixingSubgroup_insert_iff, mem_fixingSubgroup_union_iff, mem_ofFixingSubgroup_iff, mem_ofFixingSubgroup_insert_iff, not_mem_of_mem_ofFixingSubgroup, append_left, append_right, ofFixingSubgroupEmpty_equivariantMap_bijective, ofFixingSubgroup_carrier, ofFixingSubgroup_equivariantMap_injective, ofFixingSubgroup_insert_map_apply, ofFixingSubgroup_insert_map_bijective, ofFixingSubgroup_of_eq_apply, ofFixingSubgroup_of_eq_bijective, ofFixingSubgroup_of_inclusion_injective, ofFixingSubgroup_of_singleton_bijective, of_fixingSubgroupEmpty_mapScalars_surjective	58
Total	83

AddAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fixingAddSubgroup_le_stabilizer 📖	mathematical	—	AddSubgroup Preorder.toLE PartialOrder.toPreorder AddSubgroup.instPartialOrder fixingAddSubgroup stabilizer Set Set.addActionSet SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	mem_stabilizer_iff Set.image_id Set.image_congr mem_fixingAddSubgroup_iff

AddAut

Definitions

Name	Category	Theorems
instAddGroup 📖	CompOp	4 math math: Set.conj_mem_fixingAddSubgroup, SubAddAction.fixingAddSubgroup_vadd_eq_fixingAddSubgroup_map_conj, SubAddAction.fixingAddSubgroupEquivFixingAddSubgroup_coe_apply, SubAddAction.fixingAddSubgroup_map_conj_eq

MulAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fixingSubgroup_le_stabilizer 📖	mathematical	—	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder fixingSubgroup stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid	—	mem_stabilizer_iff Set.image_id Set.image_congr

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conj_mem_fixingAddSubgroup 📖	mathematical	HVAdd.hVAdd Set instHVAdd vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup	DFunLike.coe AddEquiv AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass EquivLike.toFunLike AddEquiv.instEquivLike AddMonoidHom AddAut AddAut.instAddGroup AddMonoidHom.instFunLike AddAut.conj	—	mem_fixingAddSubgroup_iff AddAut.conj_apply AddSemigroupAction.add_vadd neg_vadd_eq_iff mem_vadd_set_iff_neg_vadd_mem
conj_mem_fixingSubgroup 📖	mathematical	Set smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup	DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass EquivLike.toFunLike MulEquiv.instEquivLike MonoidHom MulAut MulAut.instGroup MonoidHom.instFunLike MulAut.conj	—	MulAut.conj_apply SemigroupAction.mul_smul inv_smul_eq_iff mem_smul_set_iff_inv_smul_mem

SubAddAction

Definitions

Name	Category	Theorems
conjMap_ofFixingAddSubgroup 📖	CompOp	2 math math: conjMap_ofFixingAddSubgroup_bijective, conjMap_ofFixingAddSubgroup_coe_apply
fixingAddSubgroupEquivFixingAddSubgroup 📖	CompOp	3 math math: conjMap_ofFixingAddSubgroup_bijective, conjMap_ofFixingAddSubgroup_coe_apply, fixingAddSubgroupEquivFixingAddSubgroup_coe_apply
fixingAddSubgroupInsertEquiv 📖	CompOp	2 math math: ofFixingAddSubgroup_insert_map_bijective, ofFixingAddSubgroup_insert_map_apply
fixingAddSubgroup_union_to_fixingAddSubgroup_of_fixingAddSubgroup 📖	CompOp	—
map_ofFixingAddSubgroupUnion 📖	CompOp	2 math math: map_ofFixingAddSubgroupUnion_bijective, map_ofFixingAddSubgroupUnion_def
ofFixingAddSubgroup 📖	CompOp	25 math math: map_ofFixingAddSubgroupUnion_bijective, ofFixingAddSubgroup_of_inclusion_injective, ofFixingAddSubgroup_of_singleton_bijective, AddAction.isPreprimitive_ofFixingAddSubgroup_conj_iff, ofFixingAddSubgroup.isMultiplyPretransitive, ofFixingAddSubgroup.isMultiplyPretransitive', conjMap_ofFixingAddSubgroup_bijective, conjMap_ofFixingAddSubgroup_coe_apply, ofFixingAddSubgroup_of_eq_bijective, ofFixingAddSubgroup_insert_map_bijective, ofFixingAddSubgroup_of_eq_apply, mem_ofFixingAddSubgroup_iff, ofFixingAddSubgroupEmpty_equivariantMap_bijective, ofFixingAddSubgroup_carrier, AddAction.isMultiplyPreprimitive_iff, ofFixingAddSubgroup.append_right, ofFixingAddSubgroup_equivariantMap_injective, AddAction.ofFixingSubgroup.isMultiplyPreprimitive, AddAction.IsMultiplyPreprimitive.isPreprimitive_ofFixingAddSubgroup, disjoint_val_image, AddAction.isPreprimitive_fixingAddSubgroup_insert_iff, mem_ofFixingAddSubgroup_insert_iff, AddAction.isPreprimitive_of_fixingAddSubgroup_empty_iff, not_mem_of_mem_ofFixingAddSubgroup, map_ofFixingAddSubgroupUnion_def
ofFixingAddSubgroup_equivariantMap 📖	CompOp	2 math math: ofFixingAddSubgroupEmpty_equivariantMap_bijective, ofFixingAddSubgroup_equivariantMap_injective
ofFixingAddSubgroup_insert_map 📖	CompOp	2 math math: ofFixingAddSubgroup_insert_map_bijective, ofFixingAddSubgroup_insert_map_apply
ofFixingAddSubgroup_of_eq 📖	CompOp	2 math math: ofFixingAddSubgroup_of_eq_bijective, ofFixingAddSubgroup_of_eq_apply
ofFixingAddSubgroup_of_inclusion 📖	CompOp	1 math math: ofFixingAddSubgroup_of_inclusion_injective
ofFixingAddSubgroup_of_singleton 📖	CompOp	1 math math: ofFixingAddSubgroup_of_singleton_bijective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conjMap_ofFixingAddSubgroup_bijective 📖	mathematical	HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	Function.Bijective SubAddAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup AddSubgroup.toAddGroup AddSubgroup.instAddAction instSetLike ofFixingAddSubgroup DFunLike.coe AddActionHom AddEquiv AddSubgroup.add EquivLike.toFunLike AddEquiv.instEquivLike fixingAddSubgroupEquivFixingAddSubgroup vadd' AddMonoid.toAddAction VAddAssocClass.left instFunLikeAddActionHom conjMap_ofFixingAddSubgroup	—	VAddAssocClass.left SetLike.coe_eq_coe vadd_left_cancel_iff neg_vadd_eq_iff vadd_neg_vadd
conjMap_ofFixingAddSubgroup_coe_apply 📖	mathematical	HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	SubAddAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup AddSubgroup.toAddGroup AddSubgroup.instAddAction instSetLike ofFixingAddSubgroup DFunLike.coe AddActionHom AddEquiv AddSubgroup.add EquivLike.toFunLike AddEquiv.instEquivLike fixingAddSubgroupEquivFixingAddSubgroup vadd' AddMonoid.toAddAction VAddAssocClass.left instFunLikeAddActionHom conjMap_ofFixingAddSubgroup	—	VAddAssocClass.left
disjoint_val_image 📖	mathematical	—	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.image SubAddAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.toAddSemigroupAction AddSubgroup.instAddAction instSetLike ofFixingAddSubgroup	—	Set.disjoint_iff Subtype.prop
fixingAddSubgroupEquivFixingAddSubgroup_coe_apply 📖	mathematical	HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup DFunLike.coe AddEquiv AddSubgroup.add EquivLike.toFunLike AddEquiv.instEquivLike fixingAddSubgroupEquivFixingAddSubgroup AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom AddAut AddAut.instAddGroup AddMonoidHom.instFunLike AddAut.conj	—	—
fixingAddSubgroup_map_conj_eq 📖	mathematical	HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	AddSubgroup.map AddEquiv.toAddMonoidHom AddMonoid.toAddZeroClass DFunLike.coe AddMonoidHom AddAut AddZero.toAdd AddZeroClass.toAddZero AddAut.instAddGroup AddMonoidHom.instFunLike AddAut.conj fixingAddSubgroup	—	AddSubgroup.ext AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass AddSubgroup.mem_map Set.conj_mem_fixingAddSubgroup neg_vadd_eq_iff neg_neg neg_one_zsmul add_assoc one_add_zsmul add_neg_cancel zero_zsmul zero_add Mathlib.Tactic.Group.zsmul_trick_zero neg_add_cancel add_zero
fixingAddSubgroup_of_insert 📖	mathematical	—	fixingAddSubgroup Set Set.instInsert 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 AddSubgroup.map AddSubgroup.subtype addAction	—	AddSubgroup.ext mem_ofStabilizer_iff mem_fixingAddSubgroup_iff Set.mem_insert_iff Set.mem_image AddSubgroup.mem_map VAddMemClass.vadd_mem instVAddMemClass AddAction.mem_stabilizer_iff
fixingAddSubgroup_vadd_eq_fixingAddSubgroup_map_conj 📖	mathematical	—	fixingAddSubgroup HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddSubgroup.map AddEquiv.toAddMonoidHom AddMonoid.toAddZeroClass DFunLike.coe AddMonoidHom AddAut AddZero.toAdd AddZeroClass.toAddZero AddAut.instAddGroup AddMonoidHom.instFunLike AddAut.conj	—	fixingAddSubgroup_map_conj_eq
map_ofFixingAddSubgroupUnion_bijective 📖	mathematical	—	Function.Bijective SubAddAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup Set Set.instUnion AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.toAddSemigroupAction AddSubgroup.instAddAction instSetLike ofFixingAddSubgroup addAction Set.preimage DFunLike.coe instFunLikeAddActionHom vadd' AddMonoid.toAddAction VAddAssocClass.left AddSubgroup.instVAddAssocClassSubtypeMem vaddAssocClass' map_ofFixingAddSubgroupUnion	—	VAddAssocClass.left AddSubgroup.instVAddAssocClassSubtypeMem vaddAssocClass' SetLike.coe_eq_coe Set.mem_union Set.mem_preimage
map_ofFixingAddSubgroupUnion_def 📖	mathematical	—	SubAddAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.toAddSemigroupAction AddSubgroup.instAddAction instSetLike ofFixingAddSubgroup addAction Set.preimage DFunLike.coe Set Set.instUnion instFunLikeAddActionHom vadd' AddMonoid.toAddAction VAddAssocClass.left AddSubgroup.instVAddAssocClassSubtypeMem vaddAssocClass' map_ofFixingAddSubgroupUnion	—	VAddAssocClass.left AddSubgroup.instVAddAssocClassSubtypeMem vaddAssocClass'
mem_fixingAddSubgroup_insert_iff 📖	mathematical	—	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup Set Set.instInsert HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	—	mem_fixingAddSubgroup_iff Set.mem_insert_iff
mem_fixingAddSubgroup_union_iff 📖	mathematical	—	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup Set Set.instUnion	—	fixingAddSubgroup_union AddSubgroup.mem_inf
mem_ofFixingAddSubgroup_iff 📖	mathematical	—	SubAddAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.toAddSemigroupAction AddSubgroup.instAddAction instSetLike ofFixingAddSubgroup Set Set.instMembership	—	—
mem_ofFixingAddSubgroup_insert_iff 📖	mathematical	—	SubAddAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup Set Set.instInsert Set.image AddAction.stabilizer AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.toAddSemigroupAction AddSubgroup.instAddAction instSetLike ofStabilizer ofFixingAddSubgroup addAction	—	—
not_mem_of_mem_ofFixingAddSubgroup 📖	mathematical	—	Set Set.instMembership SubAddAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.toAddSemigroupAction AddSubgroup.instAddAction instSetLike ofFixingAddSubgroup	—	Subtype.prop
ofFixingAddSubgroupEmpty_equivariantMap_bijective 📖	mathematical	—	Function.Bijective SubAddAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup Set Set.instEmptyCollection AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.toAddSemigroupAction AddSubgroup.instAddAction instSetLike ofFixingAddSubgroup DFunLike.coe AddActionHom AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike AddSubgroup.subtype vadd' AddMonoid.toAddAction VAddAssocClass.left instFunLikeAddActionHom ofFixingAddSubgroup_equivariantMap	—	VAddAssocClass.left ofFixingAddSubgroup_equivariantMap_injective mem_ofFixingAddSubgroup_iff Set.notMem_empty
ofFixingAddSubgroup_carrier 📖	mathematical	—	carrier AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.toAddSemigroupAction AddSubgroup.instAddAction ofFixingAddSubgroup Compl.compl Set Set.instCompl	—	—
ofFixingAddSubgroup_equivariantMap_injective 📖	mathematical	—	SubAddAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.toAddSemigroupAction AddSubgroup.instAddAction instSetLike ofFixingAddSubgroup DFunLike.coe AddActionHom AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike AddSubgroup.subtype vadd' AddMonoid.toAddAction VAddAssocClass.left instFunLikeAddActionHom ofFixingAddSubgroup_equivariantMap	—	VAddAssocClass.left
ofFixingAddSubgroup_insert_map_apply 📖	mathematical	SubAddAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup Set Set.instInsert Set.image AddAction.stabilizer AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.toAddSemigroupAction AddSubgroup.instAddAction instSetLike ofStabilizer ofFixingAddSubgroup	addAction DFunLike.coe AddActionHom AddEquiv AddSubgroup.add EquivLike.toFunLike AddEquiv.instEquivLike fixingAddSubgroupInsertEquiv vadd' AddMonoid.toAddAction VAddAssocClass.left AddSubgroup.instVAddAssocClassSubtypeMem vaddAssocClass' instFunLikeAddActionHom ofFixingAddSubgroup_insert_map	—	VAddAssocClass.left AddSubgroup.instVAddAssocClassSubtypeMem vaddAssocClass'
ofFixingAddSubgroup_insert_map_bijective 📖	mathematical	—	Function.Bijective SubAddAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup Set Set.instInsert Set.image AddAction.stabilizer AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.toAddSemigroupAction AddSubgroup.instAddAction instSetLike ofStabilizer ofFixingAddSubgroup addAction DFunLike.coe AddActionHom AddEquiv AddSubgroup.add EquivLike.toFunLike AddEquiv.instEquivLike fixingAddSubgroupInsertEquiv vadd' AddMonoid.toAddAction VAddAssocClass.left AddSubgroup.instVAddAssocClassSubtypeMem vaddAssocClass' instFunLikeAddActionHom ofFixingAddSubgroup_insert_map	—	VAddAssocClass.left AddSubgroup.instVAddAssocClassSubtypeMem vaddAssocClass' mem_ofFixingAddSubgroup_insert_iff
ofFixingAddSubgroup_of_eq_apply 📖	mathematical	—	SubAddAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.toAddSemigroupAction AddSubgroup.instAddAction instSetLike ofFixingAddSubgroup DFunLike.coe instFunLikeAddActionHom AddEquiv AddSubgroup.add EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.addSubgroupCongr AddAction Set vadd' AddMonoid.toAddAction VAddAssocClass.left ofFixingAddSubgroup_of_eq	—	VAddAssocClass.left
ofFixingAddSubgroup_of_eq_bijective 📖	mathematical	—	Function.Bijective SubAddAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.toAddSemigroupAction AddSubgroup.instAddAction instSetLike ofFixingAddSubgroup DFunLike.coe instFunLikeAddActionHom AddEquiv AddSubgroup.add EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.addSubgroupCongr AddAction Set vadd' AddMonoid.toAddAction VAddAssocClass.left ofFixingAddSubgroup_of_eq	—	VAddAssocClass.left SetLike.coe_eq_coe
ofFixingAddSubgroup_of_inclusion_injective 📖	mathematical	Set Set.instHasSubset	SubAddAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.toAddSemigroupAction AddSubgroup.instAddAction instSetLike ofFixingAddSubgroup DFunLike.coe AddActionHom AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike AddSubgroup.inclusion fixingAddSubgroup_antitone vadd' AddMonoid.toAddAction VAddAssocClass.left instFunLikeAddActionHom ofFixingAddSubgroup_of_inclusion	—	fixingAddSubgroup_antitone VAddAssocClass.left SetLike.coe_eq_coe
ofFixingAddSubgroup_of_singleton_bijective 📖	mathematical	—	Function.Bijective SubAddAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup Set Set.instSingletonSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.toAddSemigroupAction AddSubgroup.instAddAction instSetLike ofFixingAddSubgroup AddAction.stabilizer ofStabilizer DFunLike.coe instFunLikeAddActionHom mem_fixingAddSubgroup_iff Set.mem_singleton vadd' AddMonoid.toAddAction VAddAssocClass.left ofFixingAddSubgroup_of_singleton	—	mem_fixingAddSubgroup_iff Set.mem_singleton VAddAssocClass.left
of_fixingAddSubgroupEmpty_mapScalars_surjective 📖	mathematical	—	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup Set Set.instEmptyCollection DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddMonoidHom.instFunLike AddSubgroup.subtype	—	fixingAddSubgroup_empty AddSubgroup.mem_top

SubAddAction.ofFixingAddSubgroup

Definitions

Name	Category	Theorems
append 📖	CompOp	2 math math: append_left, append_right

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
append_left 📖	mathematical	—	DFunLike.coe Function.Embedding Set.ncard Function.instFunLikeEmbedding append Set Set.instMembership Equiv Set.Elem EquivLike.toFunLike Equiv.instEquivLike Nat.card Finite.card_eq Finite.of_fintype Fin.fintype	—	Finite.card_eq Finite.of_fintype Fin.append_left
append_right 📖	mathematical	—	DFunLike.coe Function.Embedding Set.ncard Function.instFunLikeEmbedding append SubAddAction AddSubgroup SetLike.instMembership AddSubgroup.instSetLike fixingAddSubgroup AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddAction.toAddSemigroupAction AddSubgroup.instAddAction SubAddAction.instSetLike SubAddAction.ofFixingAddSubgroup	—	Fin.append_right

SubMulAction

Definitions

Name	Category	Theorems
conjMap_ofFixingSubgroup 📖	CompOp	2 math math: conjMap_ofFixingSubgroup_bijective, conjMap_ofFixingSubgroup_coe_apply
fixingSubgroupEquivFixingSubgroup 📖	CompOp	3 math math: fixingSubgroupEquivFixingSubgroup_coe_apply, conjMap_ofFixingSubgroup_bijective, conjMap_ofFixingSubgroup_coe_apply
fixingSubgroupInsertEquiv 📖	CompOp	2 math math: ofFixingSubgroup_insert_map_apply, ofFixingSubgroup_insert_map_bijective
fixingSubgroup_union_to_fixingSubgroup_of_fixingSubgroup 📖	CompOp	—
map_ofFixingSubgroupUnion 📖	CompOp	2 math math: map_ofFixingSubgroupUnion_def, map_ofFixingSubgroupUnion_bijective
ofFixingSubgroup 📖	CompOp	28 math math: MulAction.isPreprimitive_of_fixingSubgroup_empty_iff, ofFixingSubgroup_equivariantMap_injective, ofFixingSubgroup_of_inclusion_injective, map_ofFixingSubgroupUnion_def, MulAction.ofFixingSubgroup.isMultiplyPreprimitive, ofFixingSubgroup_carrier, MulAction.isPreprimitive_ofFixingSubgroup_conj_iff, disjoint_val_image, MulAction.isPreprimitive_fixingSubgroup_insert_iff, ofFixingSubgroup_of_eq_apply, ofFixingSubgroup.isMultiplyPretransitive, MulAction.IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup, MulAction.isMultiplyPreprimitive_iff, mem_ofFixingSubgroup_insert_iff, Equiv.Perm.isPretransitive_of_isCycle_mem, ofFixingSubgroup.append_right, ofFixingSubgroup_of_singleton_bijective, ofFixingSubgroupEmpty_equivariantMap_bijective, map_ofFixingSubgroupUnion_bijective, ofFixingSubgroup_of_eq_bijective, not_mem_of_mem_ofFixingSubgroup, IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter, mem_ofFixingSubgroup_iff, ofFixingSubgroup.isMultiplyPretransitive', ofFixingSubgroup_insert_map_bijective, conjMap_ofFixingSubgroup_bijective, IsPretransitive.isPretransitive_ofFixingSubgroup_inter, conjMap_ofFixingSubgroup_coe_apply
ofFixingSubgroup_equivariantMap 📖	CompOp	2 math math: ofFixingSubgroup_equivariantMap_injective, ofFixingSubgroupEmpty_equivariantMap_bijective
ofFixingSubgroup_insert_map 📖	CompOp	2 math math: ofFixingSubgroup_insert_map_apply, ofFixingSubgroup_insert_map_bijective
ofFixingSubgroup_of_eq 📖	CompOp	2 math math: ofFixingSubgroup_of_eq_apply, ofFixingSubgroup_of_eq_bijective
ofFixingSubgroup_of_inclusion 📖	CompOp	1 math math: ofFixingSubgroup_of_inclusion_injective
ofFixingSubgroup_of_singleton 📖	CompOp	1 math math: ofFixingSubgroup_of_singleton_bijective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conjMap_ofFixingSubgroup_bijective 📖	mathematical	Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	Function.Bijective SubMulAction Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup Subgroup.toGroup Subgroup.instMulAction instSetLike ofFixingSubgroup DFunLike.coe MulActionHom MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike fixingSubgroupEquivFixingSubgroup smul' Monoid.toMulAction IsScalarTower.left instFunLikeMulActionHom conjMap_ofFixingSubgroup	—	IsScalarTower.left inv_smul_eq_iff smul_inv_smul
conjMap_ofFixingSubgroup_coe_apply 📖	mathematical	Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	SubMulAction Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup Subgroup.toGroup Subgroup.instMulAction instSetLike ofFixingSubgroup DFunLike.coe MulActionHom MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike fixingSubgroupEquivFixingSubgroup smul' Monoid.toMulAction IsScalarTower.left instFunLikeMulActionHom conjMap_ofFixingSubgroup	—	IsScalarTower.left
disjoint_val_image 📖	mathematical	—	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.image SubMulAction Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction instSetLike ofFixingSubgroup	—	Set.disjoint_iff Subtype.prop
fixingSubgroupEquivFixingSubgroup_coe_apply 📖	mathematical	Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup DFunLike.coe MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike fixingSubgroupEquivFixingSubgroup MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom MulAut MulAut.instGroup MonoidHom.instFunLike MulAut.conj	—	—
fixingSubgroup_map_conj_eq 📖	mathematical	Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	Subgroup.map MulEquiv.toMonoidHom Monoid.toMulOneClass DFunLike.coe MonoidHom MulAut MulOne.toMul MulOneClass.toMulOne MulAut.instGroup MonoidHom.instFunLike MulAut.conj fixingSubgroup	—	Subgroup.ext MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass Set.conj_mem_fixingSubgroup inv_smul_eq_iff inv_inv add_neg_cancel zpow_zero one_mul Mathlib.Tactic.Group.zpow_trick_one neg_add_cancel mul_one
fixingSubgroup_of_insert 📖	mathematical	—	fixingSubgroup Set Set.instInsert 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 Subgroup.map Subgroup.subtype mulAction	—	Subgroup.ext SMulMemClass.smul_mem instSMulMemClass
fixingSubgroup_smul_eq_fixingSubgroup_map_conj 📖	mathematical	—	fixingSubgroup Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Subgroup.map MulEquiv.toMonoidHom Monoid.toMulOneClass DFunLike.coe MonoidHom MulAut MulOne.toMul MulOneClass.toMulOne MulAut.instGroup MonoidHom.instFunLike MulAut.conj	—	fixingSubgroup_map_conj_eq
map_ofFixingSubgroupUnion_bijective 📖	mathematical	—	Function.Bijective SubMulAction Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup Set Set.instUnion SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction instSetLike ofFixingSubgroup mulAction Set.preimage DFunLike.coe instFunLikeMulActionHom smul' Monoid.toMulAction IsScalarTower.left Subgroup.instIsScalarTowerSubtypeMem isScalarTower' map_ofFixingSubgroupUnion	—	IsScalarTower.left Subgroup.instIsScalarTowerSubtypeMem isScalarTower' Set.mem_union
map_ofFixingSubgroupUnion_def 📖	mathematical	—	SubMulAction Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction instSetLike ofFixingSubgroup mulAction Set.preimage DFunLike.coe Set Set.instUnion instFunLikeMulActionHom smul' Monoid.toMulAction IsScalarTower.left Subgroup.instIsScalarTowerSubtypeMem isScalarTower' map_ofFixingSubgroupUnion	—	IsScalarTower.left Subgroup.instIsScalarTowerSubtypeMem isScalarTower'
mem_fixingSubgroup_insert_iff 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup Set Set.instInsert SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	—
mem_fixingSubgroup_union_iff 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup Set Set.instUnion	—	fixingSubgroup_union
mem_ofFixingSubgroup_iff 📖	mathematical	—	SubMulAction Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction instSetLike ofFixingSubgroup Set Set.instMembership	—	—
mem_ofFixingSubgroup_insert_iff 📖	mathematical	—	SubMulAction Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup Set Set.instInsert Set.image MulAction.stabilizer SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction instSetLike ofStabilizer ofFixingSubgroup mulAction	—	—
not_mem_of_mem_ofFixingSubgroup 📖	mathematical	—	Set Set.instMembership SubMulAction Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction instSetLike ofFixingSubgroup	—	Subtype.prop
ofFixingSubgroupEmpty_equivariantMap_bijective 📖	mathematical	—	Function.Bijective SubMulAction Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup Set Set.instEmptyCollection SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction instSetLike ofFixingSubgroup DFunLike.coe MulActionHom MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike Subgroup.subtype smul' Monoid.toMulAction IsScalarTower.left instFunLikeMulActionHom ofFixingSubgroup_equivariantMap	—	IsScalarTower.left ofFixingSubgroup_equivariantMap_injective mem_ofFixingSubgroup_iff Set.notMem_empty
ofFixingSubgroup_carrier 📖	mathematical	—	carrier Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction ofFixingSubgroup Compl.compl Set Set.instCompl	—	—
ofFixingSubgroup_equivariantMap_injective 📖	mathematical	—	SubMulAction Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction instSetLike ofFixingSubgroup DFunLike.coe MulActionHom MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike Subgroup.subtype smul' Monoid.toMulAction IsScalarTower.left instFunLikeMulActionHom ofFixingSubgroup_equivariantMap	—	IsScalarTower.left
ofFixingSubgroup_insert_map_apply 📖	mathematical	SubMulAction Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup Set Set.instInsert Set.image MulAction.stabilizer SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction instSetLike ofStabilizer ofFixingSubgroup	mulAction DFunLike.coe MulActionHom MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike fixingSubgroupInsertEquiv smul' Monoid.toMulAction IsScalarTower.left Subgroup.instIsScalarTowerSubtypeMem isScalarTower' instFunLikeMulActionHom ofFixingSubgroup_insert_map	—	IsScalarTower.left Subgroup.instIsScalarTowerSubtypeMem isScalarTower'
ofFixingSubgroup_insert_map_bijective 📖	mathematical	—	Function.Bijective SubMulAction Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup Set Set.instInsert Set.image MulAction.stabilizer SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction instSetLike ofStabilizer ofFixingSubgroup mulAction DFunLike.coe MulActionHom MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike fixingSubgroupInsertEquiv smul' Monoid.toMulAction IsScalarTower.left Subgroup.instIsScalarTowerSubtypeMem isScalarTower' instFunLikeMulActionHom ofFixingSubgroup_insert_map	—	IsScalarTower.left Subgroup.instIsScalarTowerSubtypeMem isScalarTower' mem_ofFixingSubgroup_insert_iff
ofFixingSubgroup_of_eq_apply 📖	mathematical	—	SubMulAction Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction instSetLike ofFixingSubgroup DFunLike.coe instFunLikeMulActionHom MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.subgroupCongr MulAction Set smul' Monoid.toMulAction IsScalarTower.left ofFixingSubgroup_of_eq	—	IsScalarTower.left
ofFixingSubgroup_of_eq_bijective 📖	mathematical	—	Function.Bijective SubMulAction Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction instSetLike ofFixingSubgroup DFunLike.coe instFunLikeMulActionHom MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.subgroupCongr MulAction Set smul' Monoid.toMulAction IsScalarTower.left ofFixingSubgroup_of_eq	—	IsScalarTower.left
ofFixingSubgroup_of_inclusion_injective 📖	mathematical	Set Set.instHasSubset	SubMulAction Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction instSetLike ofFixingSubgroup DFunLike.coe MulActionHom MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike Subgroup.inclusion fixingSubgroup_antitone smul' Monoid.toMulAction IsScalarTower.left instFunLikeMulActionHom ofFixingSubgroup_of_inclusion	—	fixingSubgroup_antitone IsScalarTower.left SetLike.coe_eq_coe
ofFixingSubgroup_of_singleton_bijective 📖	mathematical	—	Function.Bijective SubMulAction Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup Set Set.instSingletonSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction instSetLike ofFixingSubgroup MulAction.stabilizer ofStabilizer DFunLike.coe instFunLikeMulActionHom mem_fixingSubgroup_iff Set.mem_singleton smul' Monoid.toMulAction IsScalarTower.left ofFixingSubgroup_of_singleton	—	mem_fixingSubgroup_iff Set.mem_singleton IsScalarTower.left
of_fixingSubgroupEmpty_mapScalars_surjective 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup Set Set.instEmptyCollection DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidHom.instFunLike Subgroup.subtype	—	fixingSubgroup_empty

SubMulAction.IsPreprimitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPreprimitive_ofFixingSubgroup_inter 📖	mathematical	—	MulAction.IsPreprimitive Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup Set Set.instInter Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction SubMulAction Subgroup.toGroup Subgroup.instMulAction SubMulAction.instSetLike SubMulAction.ofFixingSubgroup SubMulAction.smul' Monoid.toMulAction IsScalarTower.left	—	IsScalarTower.left SubMulAction.IsPretransitive.isPretransitive_ofFixingSubgroup_inter MulAction.IsPreprimitive.toIsPretransitive MulAction.IsPreprimitive.of_card_lt fixingSubgroup_antitone Set.inter_subset_left Subtype.finite Nat.card_coe_set_eq Set.ncard_range_of_injective SubMulAction.ofFixingSubgroup_of_inclusion_injective Set.compl_inter LT.lt.trans_le Set.ncard_union_lt Set.toFinite Set.disjoint_compl_right_iff_subset Set.compl_subset_iff_union Set.smul_set_compl Set.ncard_smul_set Nat.instAtLeastTwoHAddOfNat two_mul le_refl

SubMulAction.IsPretransitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPretransitive_ofFixingSubgroup_inter 📖	mathematical	—	MulAction.IsPretransitive Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup Set Set.instInter Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction SubMulAction Subgroup.toGroup Subgroup.instMulAction SubMulAction.instSetLike SubMulAction.ofFixingSubgroup SubMulAction.smul' Monoid.toMulAction IsScalarTower.left	—	IsScalarTower.left Set.nonempty_iff_ne_empty Set.compl_empty_iff Set.top_eq_univ Set.compl_inter Set.mem_union_left Set.compl_union MulAction.isPretransitive_iff_base not_and_or Set.mem_inter_iff SubMulAction.mem_ofFixingSubgroup_iff MulAction.IsPretransitive.exists_smul_eq Set.mem_smul_set_iff_inv_smul_mem mem_fixingSubgroup_iff SemigroupAction.mul_smul smul_eq_iff_eq_inv_smul smul_smul eq_inv_smul_iff Subgroup.mk_smul SubMulAction.instSMulMemClass SetLike.val_smul

SubMulAction.ofFixingSubgroup

Definitions

Name	Category	Theorems
append 📖	CompOp	2 math math: append_left, append_right

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
append_left 📖	mathematical	—	DFunLike.coe Function.Embedding Set.ncard Function.instFunLikeEmbedding append Set Set.instMembership Equiv Set.Elem EquivLike.toFunLike Equiv.instEquivLike Nat.card Finite.card_eq Finite.of_fintype Fin.fintype	—	Finite.card_eq Finite.of_fintype Fin.append_left
append_right 📖	mathematical	—	DFunLike.coe Function.Embedding Set.ncard Function.instFunLikeEmbedding append SubMulAction Subgroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction SubMulAction.instSetLike SubMulAction.ofFixingSubgroup	—	Fin.append_right

---

← Back to Index