Actions

📁 Source: Mathlib/Algebra/Group/Subgroup/Actions.lean

Statistics

Metric	Count
Definitions instAddAction, instDistribMulActionSubtypeMem, instMulAction, instMulDistribMulActionSubtypeMem	4
Theorems instFaithfulVAddSubtypeMem, instVAddAssocClassSubtypeMem, mk_vadd, vaddCommClass_left, vaddCommClass_right, vadd_def, smulCommClass_left, smulCommClass_right, instFaithfulSMulSubtypeMem, instIsScalarTowerSubtypeMem, mk_smul, smulCommClass_left, smulCommClass_right, smul_def	14
Total	18

AddSubgroup

Definitions

Name	Category	Theorems
instAddAction 📖	CompOp	78 math math: SubAddAction.map_ofFixingAddSubgroupUnion_bijective, SubAddAction.notMem_val_image, AddCircle.isAddQuotientCoveringMap_zsmul_of_ne_zero, vaddCommClass_left, SubAddAction.ofStabilizer.conjMap_comp, SubAddAction.ofFixingAddSubgroup_of_inclusion_injective, SubAddAction.ofFixingAddSubgroup_of_singleton_bijective, AddCircle.isAddQuotientCoveringMap_nsmul_of_ne_zero, AddCircle.isAddQuotientCoveringMap_nsmul, SubAddAction.mem_ofStabilizer_iff, SubAddAction.ofStabilizer.isMultiplyPretransitive_iff_of_conj, Topology.IsQuotientMap.isAddQuotientCoveringMap_of_addSubgroupOp, AddCircle.isAddQuotientCoveringMap_coe, AddAction.isPreprimitive_ofFixingAddSubgroup_conj_iff, vaddCommClass_right, AddAction.IsBlock.of_orbit, AddAction.IsQuasiPreprimitive.isPretransitive_of_normal, SubAddAction.ofStabilizer.conjMap_comp_neg_apply, SubAddAction.ofFixingAddSubgroup.isMultiplyPretransitive, SubAddAction.ofFixingAddSubgroup.isMultiplyPretransitive', SubAddAction.ofStabilizer.isPretransitive_iff, SubAddAction.conjMap_ofFixingAddSubgroup_bijective, SubAddAction.conjMap_ofFixingAddSubgroup_coe_apply, isAddQuotientCoveringMap_of_comm, finite_quotient_of_pretransitive_of_index_ne_zero, SubAddAction.ofFixingAddSubgroup_of_eq_bijective, Topology.IsQuotientMap.isAddQuotientCoveringMap_of_addSubgroup, instMeasurableVAdd, SubAddAction.ofFixingAddSubgroup_insert_map_bijective, AddAction.vadd_orbit_eq_orbit_vadd, instFaithfulVAddSubtypeMem, SubAddAction.nat_card_ofStabilizer_eq, SubAddAction.ofFixingAddSubgroup_of_eq_apply, instVAddAssocClassSubtypeMem, isAddQuotientCoveringMap, instMeasurableConstVAdd, SubAddAction.ofStabilizer.isMultiplyPretransitive_iff, finite_quotient_of_finite_quotient_of_index_ne_zero, AddAction.isBlock_top, SubAddAction.ofStabilizer.conjMap_bijective, MeasureTheory.Subgroup.vaddInvariantMeasure, vadd_def, Topology.IsQuotientMap.isAddQuotientCoveringMap_of_isDiscrete_ker_addMonoidHom, AddAction.isMultiplyPreprimitive_succ_iff_ofStabilizer, SubAddAction.ofStabilizer.snoc_castSucc, SubAddAction.ENat_card_ofStabilizer_add_zero_eq, SubAddAction.fixingAddSubgroup_of_insert, SubAddAction.mem_ofFixingAddSubgroup_iff, SubAddAction.ofFixingAddSubgroupEmpty_equivariantMap_bijective, AddAction.IsBlock.orbit_stabilizer_eq, SubAddAction.ofFixingAddSubgroup_carrier, SubAddAction.ofStabilizer.neg_conjMap_comp_apply, AddCircle.isAddQuotientCoveringMap_zsmul, mk_vadd, AddAction.isMultiplyPreprimitive_iff, AddAction.IsBlock.addSubgroup, SubAddAction.ofFixingAddSubgroup.append_right, SubAddAction.ofFixingAddSubgroup_equivariantMap_injective, AddAction.ofFixingSubgroup.isMultiplyPreprimitive, SubAddAction.nat_card_ofStabilizer_add_zero_eq, AddAction.IsMultiplyPreprimitive.isPreprimitive_ofFixingAddSubgroup, SubAddAction.ofStabilizer_carrier, SubAddAction.disjoint_val_image, properlyDiscontinuousVAdd_of_tendsto_cofinite, SubAddAction.ofStabilizer.conjMap_comp_apply, SubAddAction.ofStabilizer.isMultiplyPretransitive, AddAction.stabilizer_orbit_eq, AddAction.isPreprimitive_fixingAddSubgroup_insert_iff, AddAction.isMultiplyPreprimitive_ofStabilizer, SubAddAction.mem_ofFixingAddSubgroup_insert_iff, AddAction.isPreprimitive_of_fixingAddSubgroup_empty_iff, IsAddQuotientCoveringMap.addSubgroup_congr, AddAction.IsBlock.orbit_of_normal, SubAddAction.not_mem_of_mem_ofFixingAddSubgroup, AddAction.IsBlockSystem.of_normal, SubAddAction.ofStabilizer.isPretransitive_iff_of_conj, SubAddAction.map_ofFixingAddSubgroupUnion_def, SubAddAction.ofStabilizer.conjMap_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulVAddSubtypeMem 📖	mathematical	—	FaithfulVAdd AddSubgroup SetLike.instMembership instSetLike AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddGroup AddAction.toAddSemigroupAction instAddAction	—	AddSubmonoid.faithfulVAdd
instVAddAssocClassSubtypeMem 📖	mathematical	—	VAddAssocClass AddSubgroup SetLike.instMembership instSetLike AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddGroup AddAction.toAddSemigroupAction instAddAction	—	AddSubmonoid.vaddAssocClass
mk_vadd 📖	mathematical	AddSubgroup SetLike.instMembership instSetLike	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddGroup AddAction.toAddSemigroupAction instAddAction	—	—
vaddCommClass_left 📖	mathematical	—	VAddCommClass AddSubgroup SetLike.instMembership instSetLike AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddGroup AddAction.toAddSemigroupAction instAddAction	—	AddSubmonoid.vaddCommClass_left
vaddCommClass_right 📖	mathematical	—	VAddCommClass AddSubgroup SetLike.instMembership instSetLike AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddGroup AddAction.toAddSemigroupAction instAddAction	—	AddSubmonoid.vaddCommClass_right
vadd_def 📖	mathematical	—	HVAdd.hVAdd AddSubgroup SetLike.instMembership instSetLike instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddGroup AddAction.toAddSemigroupAction instAddAction	—	—

Subgroup

Definitions

Name	Category	Theorems
instDistribMulActionSubtypeMem 📖	CompOp	11 math math: RootPairing.span_orbit_eq_top, Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_symm_apply_coe_coe, RootPairing.weylGroup_apply_root, SpecialLinearGroup.centerEquivRootsOfUnity_symm_apply, Ideal.Quotient.stabilizerHom_apply, RootPairing.InvariantForm.apply_weylGroup_smul, SpecialLinearGroup.centerEquivRootsOfUnity_apply, RootPairing.weylGroup.ofIdx_smul, autEquivRootsOfUnity_apply_rootOfSplit, SpecialLinearGroup.centerEquivRootsOfUnity_apply_apply, autEquivRootsOfUnity_smul
instMulAction 📖	CompOp	94 math math: SubMulAction.ofStabilizer.isPretransitive_iff_of_conj, MulAction.isPreprimitive_of_fixingSubgroup_empty_iff, SubMulAction.ofStabilizer.conjMap_comp_apply, ModularGroup.SLOnGLPos_smul_apply, SubMulAction.ofStabilizer_carrier, MeasureTheory.Subgroup.smulInvariantMeasure, SubMulAction.ofFixingSubgroup_equivariantMap_injective, IsPGroup.sylow_mem_fixedPoints_iff, alternatingGroup.isPreprimitive_of_three_le_card, SubMulAction.ofStabilizer.conjMap_comp_inv_apply, exists_smul_eq, SubMulAction.ofFixingSubgroup_of_inclusion_injective, center.smulCommClass_right, MulAction.IsQuasiPreprimitive.isPretransitive_of_normal, SubMulAction.nat_card_ofStabilizer_add_one_eq, SubMulAction.ofStabilizer.inv_conjMap_comp_apply, smulCommClass_right, AlternatingGroup.isPreprimitive_of_three_le_card, SubMulAction.map_ofFixingSubgroupUnion_def, SubMulAction.ofStabilizer.isMultiplyPretransitive_iff, MulAction.isBlock_top, MulAction.ofFixingSubgroup.isMultiplyPreprimitive, SubMulAction.ofStabilizer.isPretransitive_iff, Topology.IsQuotientMap.isQuotientCoveringMap_of_subgroup, MulAction.IsBlock.orbit_of_normal, SubMulAction.fixingSubgroup_of_insert, SubMulAction.ofFixingSubgroup_carrier, MulAction.isPreprimitive_ofFixingSubgroup_conj_iff, ModularGroup.SL_to_GL_tower, SubMulAction.ofStabilizer.isMultiplyPretransitive_iff_of_conj, sylow_mem_fixedPoints_iff, MulAction.IsBlock.orbit_stabilizer_eq, Topology.IsQuotientMap.isQuotientCoveringMap_of_subgroupOp, SubMulAction.disjoint_val_image, SubMulAction.nat_card_ofStabilizer_eq, MulAction.isPreprimitive_fixingSubgroup_insert_iff, IsQuotientCoveringMap.subgroup_congr, SubMulAction.ofFixingSubgroup_of_eq_apply, instMeasurableConstSMul, SubMulAction.nat_card_ofStabilizer_eq_add_one, SubMulAction.ofFixingSubgroup.isMultiplyPretransitive, MulAction.isPreprimitive_stabilizer_subgroup, SubMulAction.ENat_card_ofStabilizer_add_one_eq, SubMulAction.notMem_val_image, isPretransitive_of_stabilizer_lt, instIsScalarTowerSubtypeMem, Topology.IsQuotientMap.isQuotientCoveringMap_of_isDiscrete_ker_monoidHom, MulAction.IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup, center.smulCommClass_left, MulAction.isMultiplyPreprimitive_iff, AlternatingGroup.isMultiplyPretransitive, SubMulAction.mem_ofStabilizer_iff, SubMulAction.ofStabilizer.snoc_castSucc, SubMulAction.mem_ofFixingSubgroup_insert_iff, Equiv.Perm.isPretransitive_of_isCycle_mem, MulAction.isMultiplyPreprimitive_succ_iff_ofStabilizer, SubMulAction.ofStabilizer.conjMap_comp, smul_def, instMeasurableSMul, AlternatingGroup.isPretransitive_of_three_le_card, finite_quotient_of_pretransitive_of_index_ne_zero, SubMulAction.ofStabilizer.isMultiplyPretransitive, SubMulAction.ofFixingSubgroup.append_right, isQuotientCoveringMap_of_comm, SubMulAction.ofFixingSubgroup_of_singleton_bijective, Sylow.smul_subtype, SubMulAction.ofFixingSubgroupEmpty_equivariantMap_bijective, SubMulAction.map_ofFixingSubgroupUnion_bijective, properlyDiscontinuousSMul_of_tendsto_cofinite, alternatingGroup.isPretransitive_of_three_le_card, SubMulAction.ofFixingSubgroup_of_eq_bijective, SubMulAction.not_mem_of_mem_ofFixingSubgroup, alternatingGroup.isMultiplyPretransitive, MulAction.stabilizer_orbit_eq, SubMulAction.IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter, MulAction.isMultiplyPreprimitive_ofStabilizer, finite_quotient_of_finite_quotient_of_index_ne_zero, SubMulAction.mem_ofFixingSubgroup_iff, SubMulAction.ofStabilizer.conjMap_bijective, SubMulAction.ofFixingSubgroup.isMultiplyPretransitive', Sylow.smul_le, MulAction.IsBlock.subgroup, smulCommClass_left, SubMulAction.ofStabilizer.conjMap_apply, MulAction.IsBlockSystem.of_normal, MulAction.IsBlock.of_orbit, SubMulAction.ofFixingSubgroup_insert_map_bijective, instFaithfulSMulSubtypeMem, SubMulAction.conjMap_ofFixingSubgroup_bijective, mk_smul, SubMulAction.IsPretransitive.isPretransitive_ofFixingSubgroup_inter, isQuotientCoveringMap, MulAction.smul_orbit_eq_orbit_smul, SubMulAction.conjMap_ofFixingSubgroup_coe_apply
instMulDistribMulActionSubtypeMem 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulSMulSubtypeMem 📖	mathematical	—	FaithfulSMul Subgroup SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toGroup MulAction.toSemigroupAction instMulAction	—	Submonoid.faithfulSMul
instIsScalarTowerSubtypeMem 📖	mathematical	—	IsScalarTower Subgroup SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toGroup MulAction.toSemigroupAction instMulAction	—	Submonoid.isScalarTower
mk_smul 📖	mathematical	Subgroup SetLike.instMembership instSetLike	SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toGroup MulAction.toSemigroupAction instMulAction	—	—
smulCommClass_left 📖	mathematical	—	SMulCommClass Subgroup SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toGroup MulAction.toSemigroupAction instMulAction	—	Submonoid.smulCommClass_left
smulCommClass_right 📖	mathematical	—	SMulCommClass Subgroup SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toGroup MulAction.toSemigroupAction instMulAction	—	Submonoid.smulCommClass_right
smul_def 📖	mathematical	—	Subgroup SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toGroup MulAction.toSemigroupAction instMulAction	—	—

Subgroup.center

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smulCommClass_left 📖	mathematical	—	SMulCommClass Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.center SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction Monoid.toMulAction	—	Submonoid.center.smulCommClass_left
smulCommClass_right 📖	mathematical	—	SMulCommClass Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.center SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction Subgroup.toGroup Subgroup.instMulAction	—	Submonoid.center.smulCommClass_right

---

← Back to Index